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  29017  lshpkrlem5  39574  lplnexllnN  40024  4atexlemutvt  40514  cdlemc5  40655  cdlemd2  40659  cdleme0moN  40685  cdleme3h  40695  cdleme5  40700  cdleme9  40713  cdleme11l  40729  cdleme14  40733  cdleme15c  40736  cdleme16b  40739  cdleme16d  40741  cdleme16e  40742  cdlemednpq  40759  cdleme20bN  40770  cdleme20j  40778  cdleme20l2  40781  cdleme20l  40782  cdleme22cN  40802  cdleme22d  40803  cdleme22e  40804  cdleme22f  40806  cdleme26fALTN  40822  cdleme26f  40823  cdleme26f2ALTN  40824  cdleme26f2  40825  cdleme27a  40827  cdleme32b  40902  cdleme32d  40904  cdleme32f  40906  cdleme39n  40926  cdleme40n  40928  cdlemg2fv2  41060  cdlemg17h  41128  cdlemg27b  41156  cdlemg28b  41163  cdlemg28  41164  cdlemg29  41165  cdlemg33a  41166  cdlemg33d  41169  cdlemk7u-2N  41348  cdlemk11u-2N  41349  cdlemk12u-2N  41350  cdlemk26-3  41366  cdlemk27-3  41367  cdlemkfid3N  41385  cdlemn11c  41669