Theorem simp23r 1312

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

Assertion

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

Proof of Theorem simp23r

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

Syntax hints:   → wi 4   ∧ wa 400   ∧ w3a 1101

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 210  df-an 401  df-3an 1103

This theorem is referenced by:  ax5seglem6  29193  lshpkrlem5  39750  lplnexllnN  40200  4atexlemutvt  40690  cdlemc5  40831  cdlemd2  40835  cdleme0moN  40861  cdleme3h  40871  cdleme5  40876  cdleme9  40889  cdleme11l  40905  cdleme14  40909  cdleme15c  40912  cdleme16b  40915  cdleme16d  40917  cdleme16e  40918  cdlemednpq  40935  cdleme20bN  40946  cdleme20j  40954  cdleme20l2  40957  cdleme20l  40958  cdleme22cN  40978  cdleme22d  40979  cdleme22e  40980  cdleme22f  40982  cdleme26fALTN  40998  cdleme26f  40999  cdleme26f2ALTN  41000  cdleme26f2  41001  cdleme27a  41003  cdleme32b  41078  cdleme32d  41080  cdleme32f  41082  cdleme39n  41102  cdleme40n  41104  cdlemg2fv2  41236  cdlemg17h  41304  cdlemg27b  41332  cdlemg28b  41339  cdlemg28  41340  cdlemg29  41341  cdlemg33a  41342  cdlemg33d  41345  cdlemk7u-2N  41524  cdlemk11u-2N  41525  cdlemk12u-2N  41526  cdlemk26-3  41542  cdlemk27-3  41543  cdlemkfid3N  41561  cdlemn11c  41845