Theorem simp23r 1176

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

Assertion

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

Proof of Theorem simp23r

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

Syntax hints:   → wi 4   ∧ wa 383   ∧ w3a 1031

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 196  df-an 385  df-3an 1033

This theorem is referenced by:  ax5seglem6  25614  lshpkrlem5  33419  lplnexllnN  33868  4atexlemutvt  34358  cdlemc5  34500  cdlemd2  34504  cdleme0moN  34530  cdleme3h  34540  cdleme5  34545  cdleme9  34558  cdleme11l  34574  cdleme14  34578  cdleme15c  34581  cdleme16b  34584  cdleme16d  34586  cdleme16e  34587  cdlemednpq  34604  cdleme20bN  34616  cdleme20j  34624  cdleme20l2  34627  cdleme20l  34628  cdleme22cN  34648  cdleme22d  34649  cdleme22e  34650  cdleme22f  34652  cdleme26fALTN  34668  cdleme26f  34669  cdleme26f2ALTN  34670  cdleme26f2  34671  cdleme27a  34673  cdleme32b  34748  cdleme32d  34750  cdleme32f  34752  cdleme39n  34772  cdleme40n  34774  cdlemg2fv2  34906  cdlemg17h  34974  cdlemg27b  35002  cdlemg28b  35009  cdlemg28  35010  cdlemg29  35011  cdlemg33a  35012  cdlemg33d  35015  cdlemk7u-2N  35194  cdlemk11u-2N  35195  cdlemk12u-2N  35196  cdlemk26-3  35212  cdlemk27-3  35213  cdlemkfid3N  35231  cdlemn11c  35516