Theorem simp23r 1314

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

Assertion

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

Proof of Theorem simp23r

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∧ w3a 1103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105

This theorem is used by:  ax5seglem6  29399  lshpkrlem5  39995  lplnexllnN  40445  4atexlemutvt  40935  cdlemc5  41076  cdlemd2  41080  cdleme0moN  41106  cdleme3h  41116  cdleme5  41121  cdleme9  41134  cdleme11l  41150  cdleme14  41154  cdleme15c  41157  cdleme16b  41160  cdleme16d  41162  cdleme16e  41163  cdlemednpq  41180  cdleme20bN  41191  cdleme20j  41199  cdleme20l2  41202  cdleme20l  41203  cdleme22cN  41223  cdleme22d  41224  cdleme22e  41225  cdleme22f  41227  cdleme26fALTN  41243  cdleme26f  41244  cdleme26f2ALTN  41245  cdleme26f2  41246  cdleme27a  41248  cdleme32b  41323  cdleme32d  41325  cdleme32f  41327  cdleme39n  41347  cdleme40n  41349  cdlemg2fv2  41481  cdlemg17h  41549  cdlemg27b  41577  cdlemg28b  41584  cdlemg28  41585  cdlemg29  41586  cdlemg33a  41587  cdlemg33d  41590  cdlemk7u-2N  41769  cdlemk11u-2N  41770  cdlemk12u-2N  41771  cdlemk26-3  41787  cdlemk27-3  41788  cdlemkfid3N  41806  cdlemn11c  42090