Theorem simp23r 1183

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

Assertion

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

Proof of Theorem simp23r

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

Syntax hints:   → wi 4   ∧ wa 384   ∧ w3a 1037

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 197  df-an 386  df-3an 1039

This theorem is referenced by:  ax5seglem6  25814  lshpkrlem5  34401  lplnexllnN  34850  4atexlemutvt  35340  cdlemc5  35482  cdlemd2  35486  cdleme0moN  35512  cdleme3h  35522  cdleme5  35527  cdleme9  35540  cdleme11l  35556  cdleme14  35560  cdleme15c  35563  cdleme16b  35566  cdleme16d  35568  cdleme16e  35569  cdlemednpq  35586  cdleme20bN  35598  cdleme20j  35606  cdleme20l2  35609  cdleme20l  35610  cdleme22cN  35630  cdleme22d  35631  cdleme22e  35632  cdleme22f  35634  cdleme26fALTN  35650  cdleme26f  35651  cdleme26f2ALTN  35652  cdleme26f2  35653  cdleme27a  35655  cdleme32b  35730  cdleme32d  35732  cdleme32f  35734  cdleme39n  35754  cdleme40n  35756  cdlemg2fv2  35888  cdlemg17h  35956  cdlemg27b  35984  cdlemg28b  35991  cdlemg28  35992  cdlemg29  35993  cdlemg33a  35994  cdlemg33d  35997  cdlemk7u-2N  36176  cdlemk11u-2N  36177  cdlemk12u-2N  36178  cdlemk26-3  36194  cdlemk27-3  36195  cdlemkfid3N  36213  cdlemn11c  36498