Theorem simp23r 1297

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

Assertion

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

Proof of Theorem simp23r

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

Syntax hints:   → wi 4   ∧ wa 395   ∧ 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 207  df-an 396  df-3an 1089

This theorem is referenced by:  ax5seglem6  29003  lshpkrlem5  39560  lplnexllnN  40010  4atexlemutvt  40500  cdlemc5  40641  cdlemd2  40645  cdleme0moN  40671  cdleme3h  40681  cdleme5  40686  cdleme9  40699  cdleme11l  40715  cdleme14  40719  cdleme15c  40722  cdleme16b  40725  cdleme16d  40727  cdleme16e  40728  cdlemednpq  40745  cdleme20bN  40756  cdleme20j  40764  cdleme20l2  40767  cdleme20l  40768  cdleme22cN  40788  cdleme22d  40789  cdleme22e  40790  cdleme22f  40792  cdleme26fALTN  40808  cdleme26f  40809  cdleme26f2ALTN  40810  cdleme26f2  40811  cdleme27a  40813  cdleme32b  40888  cdleme32d  40890  cdleme32f  40892  cdleme39n  40912  cdleme40n  40914  cdlemg2fv2  41046  cdlemg17h  41114  cdlemg27b  41142  cdlemg28b  41149  cdlemg28  41150  cdlemg29  41151  cdlemg33a  41152  cdlemg33d  41155  cdlemk7u-2N  41334  cdlemk11u-2N  41335  cdlemk12u-2N  41336  cdlemk26-3  41352  cdlemk27-3  41353  cdlemkfid3N  41371  cdlemn11c  41655