Theorem simp23r 1295

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

Assertion

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

Proof of Theorem simp23r

Step	Hyp	Ref	Expression
1		simp3r 1202	. 2 ⊢ ((𝜒 ∧ 𝜃 ∧ (𝜑 ∧ 𝜓)) → 𝜓)
2	1	3ad2ant2 1134	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  28967  lshpkrlem5  39070  lplnexllnN  39521  4atexlemutvt  40011  cdlemc5  40152  cdlemd2  40156  cdleme0moN  40182  cdleme3h  40192  cdleme5  40197  cdleme9  40210  cdleme11l  40226  cdleme14  40230  cdleme15c  40233  cdleme16b  40236  cdleme16d  40238  cdleme16e  40239  cdlemednpq  40256  cdleme20bN  40267  cdleme20j  40275  cdleme20l2  40278  cdleme20l  40279  cdleme22cN  40299  cdleme22d  40300  cdleme22e  40301  cdleme22f  40303  cdleme26fALTN  40319  cdleme26f  40320  cdleme26f2ALTN  40321  cdleme26f2  40322  cdleme27a  40324  cdleme32b  40399  cdleme32d  40401  cdleme32f  40403  cdleme39n  40423  cdleme40n  40425  cdlemg2fv2  40557  cdlemg17h  40625  cdlemg27b  40653  cdlemg28b  40660  cdlemg28  40661  cdlemg29  40662  cdlemg33a  40663  cdlemg33d  40666  cdlemk7u-2N  40845  cdlemk11u-2N  40846  cdlemk12u-2N  40847  cdlemk26-3  40863  cdlemk27-3  40864  cdlemkfid3N  40882  cdlemn11c  41166