Theorem simp23r 1302

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

Assertion

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

Proof of Theorem simp23r

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

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

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

This theorem is referenced by:  ax5seglem6  29028  lshpkrlem5  39613  lplnexllnN  40063  4atexlemutvt  40553  cdlemc5  40694  cdlemd2  40698  cdleme0moN  40724  cdleme3h  40734  cdleme5  40739  cdleme9  40752  cdleme11l  40768  cdleme14  40772  cdleme15c  40775  cdleme16b  40778  cdleme16d  40780  cdleme16e  40781  cdlemednpq  40798  cdleme20bN  40809  cdleme20j  40817  cdleme20l2  40820  cdleme20l  40821  cdleme22cN  40841  cdleme22d  40842  cdleme22e  40843  cdleme22f  40845  cdleme26fALTN  40861  cdleme26f  40862  cdleme26f2ALTN  40863  cdleme26f2  40864  cdleme27a  40866  cdleme32b  40941  cdleme32d  40943  cdleme32f  40945  cdleme39n  40965  cdleme40n  40967  cdlemg2fv2  41099  cdlemg17h  41167  cdlemg27b  41195  cdlemg28b  41202  cdlemg28  41203  cdlemg29  41204  cdlemg33a  41205  cdlemg33d  41208  cdlemk7u-2N  41387  cdlemk11u-2N  41388  cdlemk12u-2N  41389  cdlemk26-3  41405  cdlemk27-3  41406  cdlemkfid3N  41424  cdlemn11c  41708