Theorem simp23r 1295

Description: Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)

Assertion

Ref	Expression
simp23r	⊢ ((𝜏 ∧ (𝜒 ∧ 𝜃 ∧ (𝜑 ∧ 𝜓)) ∧ 𝜂) → 𝜓)

Proof of Theorem simp23r

Step	Hyp	Ref	Expression
1		simp3r 1202	. 2 ⊢ ((𝜒 ∧ 𝜃 ∧ (𝜑 ∧ 𝜓)) → 𝜓)
2	1	3ad2ant2 1134	1 ⊢ ((𝜏 ∧ (𝜒 ∧ 𝜃 ∧ (𝜑 ∧ 𝜓)) ∧ 𝜂) → 𝜓)

Syntax hints:   → wi 4   ∧ wa 396   ∧ w3a 1087

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 397  df-3an 1089

This theorem is referenced by:  ax5seglem6  27946  lshpkrlem5  37649  lplnexllnN  38100  4atexlemutvt  38590  cdlemc5  38731  cdlemd2  38735  cdleme0moN  38761  cdleme3h  38771  cdleme5  38776  cdleme9  38789  cdleme11l  38805  cdleme14  38809  cdleme15c  38812  cdleme16b  38815  cdleme16d  38817  cdleme16e  38818  cdlemednpq  38835  cdleme20bN  38846  cdleme20j  38854  cdleme20l2  38857  cdleme20l  38858  cdleme22cN  38878  cdleme22d  38879  cdleme22e  38880  cdleme22f  38882  cdleme26fALTN  38898  cdleme26f  38899  cdleme26f2ALTN  38900  cdleme26f2  38901  cdleme27a  38903  cdleme32b  38978  cdleme32d  38980  cdleme32f  38982  cdleme39n  39002  cdleme40n  39004  cdlemg2fv2  39136  cdlemg17h  39204  cdlemg27b  39232  cdlemg28b  39239  cdlemg28  39240  cdlemg29  39241  cdlemg33a  39242  cdlemg33d  39245  cdlemk7u-2N  39424  cdlemk11u-2N  39425  cdlemk12u-2N  39426  cdlemk26-3  39442  cdlemk27-3  39443  cdlemkfid3N  39461  cdlemn11c  39745