Theorem simp23r 1351

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

Assertion

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

Proof of Theorem simp23r

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

Syntax hints:   → wi 4   ∧ wa 386   ∧ 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 199  df-an 387  df-3an 1073

This theorem is referenced by:  ax5seglem6  26283  lshpkrlem5  35268  lplnexllnN  35718  4atexlemutvt  36208  cdlemc5  36349  cdlemd2  36353  cdleme0moN  36379  cdleme3h  36389  cdleme5  36394  cdleme9  36407  cdleme11l  36423  cdleme14  36427  cdleme15c  36430  cdleme16b  36433  cdleme16d  36435  cdleme16e  36436  cdlemednpq  36453  cdleme20bN  36464  cdleme20j  36472  cdleme20l2  36475  cdleme20l  36476  cdleme22cN  36496  cdleme22d  36497  cdleme22e  36498  cdleme22f  36500  cdleme26fALTN  36516  cdleme26f  36517  cdleme26f2ALTN  36518  cdleme26f2  36519  cdleme27a  36521  cdleme32b  36596  cdleme32d  36598  cdleme32f  36600  cdleme39n  36620  cdleme40n  36622  cdlemg2fv2  36754  cdlemg17h  36822  cdlemg27b  36850  cdlemg28b  36857  cdlemg28  36858  cdlemg29  36859  cdlemg33a  36860  cdlemg33d  36863  cdlemk7u-2N  37042  cdlemk11u-2N  37043  cdlemk12u-2N  37044  cdlemk26-3  37060  cdlemk27-3  37061  cdlemkfid3N  37079  cdlemn11c  37363