simpr1r - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > simpr1r		Structured version Visualization version GIF version

Theorem simpr1r 1228

Description: Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) (Proof shortened by Wolf Lammen, 24-Jun-2022.)

**Assertion**
Ref	Expression
simpr1r	⊢ ((𝜏 ∧ ((𝜑 ∧ 𝜓) ∧ 𝜒 ∧ 𝜃)) → 𝜓)

**Proof of Theorem simpr1r**
Step	Hyp	Ref	Expression
1		simprr 771	. 2 ⊢ ((𝜏 ∧ (𝜑 ∧ 𝜓)) → 𝜓)
2	1	3ad2antr1 1185	1 ⊢ ((𝜏 ∧ ((𝜑 ∧ 𝜓) ∧ 𝜒 ∧ 𝜃)) → 𝜓)

Colors of variables: wff setvar class

Syntax hints: → wi 4 ∧ wa 394 ∧ w3a 1084

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8

This theorem depends on definitions: df-bi 206 df-an 395 df-3an 1086

This theorem is referenced by: poxp2 8146 oppccatid 17701 subccatid 17832 setccatid 18073 catccatid 18095 estrccatid 18122 xpccatid 18179 gsmsymgreqlem1 19390 dmdprdsplit 20009 neitr 23115 neitx 23542 tx1stc 23585 utop3cls 24187 metustsym 24495 clwwlkccat 29857 3pthdlem1 30031 archiabllem1 32969 esumpcvgval 33784 esum2d 33799 ifscgr 35727 btwnconn1lem8 35777 btwnconn1lem11 35780 btwnconn1lem12 35781 segletr 35797 broutsideof3 35809 unbdqndv2 36073 lhp2lt 39560 cdlemf2 40121 cdlemn11pre 40769 stoweidlem60 45528 isthincd2 48172 mndtccatid 48227

	
		OSZAR »