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 8148 oppccatid 17704 subccatid 17835 setccatid 18076 catccatid 18098 estrccatid 18125 xpccatid 18182 gsmsymgreqlem1 19397 dmdprdsplit 20016 neitr 23128 neitx 23555 tx1stc 23598 utop3cls 24200 metustsym 24508 clwwlkccat 29872 3pthdlem1 30046 archiabllem1 32993 esumpcvgval 33828 esum2d 33843 ifscgr 35771 btwnconn1lem8 35821 btwnconn1lem11 35824 btwnconn1lem12 35825 segletr 35841 broutsideof3 35853 unbdqndv2 36117 lhp2lt 39604 cdlemf2 40165 cdlemn11pre 40813 stoweidlem60 45586 isthincd2 48230 mndtccatid 48285

	
		OSZAR »