Theorem simp23r 1379

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

Assertion

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

Proof of Theorem simp23r

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

Syntax hints:   → wi 4   ∧ wa 382   ∧ w3a 1071

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 383  df-3an 1073

This theorem is referenced by:  ax5seglem6  26034  lshpkrlem5  34922  lplnexllnN  35372  4atexlemutvt  35862  cdlemc5  36004  cdlemd2  36008  cdleme0moN  36034  cdleme3h  36044  cdleme5  36049  cdleme9  36062  cdleme11l  36078  cdleme14  36082  cdleme15c  36085  cdleme16b  36088  cdleme16d  36090  cdleme16e  36091  cdlemednpq  36108  cdleme20bN  36119  cdleme20j  36127  cdleme20l2  36130  cdleme20l  36131  cdleme22cN  36151  cdleme22d  36152  cdleme22e  36153  cdleme22f  36155  cdleme26fALTN  36171  cdleme26f  36172  cdleme26f2ALTN  36173  cdleme26f2  36174  cdleme27a  36176  cdleme32b  36251  cdleme32d  36253  cdleme32f  36255  cdleme39n  36275  cdleme40n  36277  cdlemg2fv2  36409  cdlemg17h  36477  cdlemg27b  36505  cdlemg28b  36512  cdlemg28  36513  cdlemg29  36514  cdlemg33a  36515  cdlemg33d  36518  cdlemk7u-2N  36697  cdlemk11u-2N  36698  cdlemk12u-2N  36699  cdlemk26-3  36715  cdlemk27-3  36716  cdlemkfid3N  36734  cdlemn11c  37019