Theorem simp23r 1378

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

Assertion

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

Proof of Theorem simp23r

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

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

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 1072

This theorem is referenced by:  ax5seglem6  26034  lshpkrlem5  34916  lplnexllnN  35365  4atexlemutvt  35855  cdlemc5  35997  cdlemd2  36001  cdleme0moN  36027  cdleme3h  36037  cdleme5  36042  cdleme9  36055  cdleme11l  36071  cdleme14  36075  cdleme15c  36078  cdleme16b  36081  cdleme16d  36083  cdleme16e  36084  cdlemednpq  36101  cdleme20bN  36112  cdleme20j  36120  cdleme20l2  36123  cdleme20l  36124  cdleme22cN  36144  cdleme22d  36145  cdleme22e  36146  cdleme22f  36148  cdleme26fALTN  36164  cdleme26f  36165  cdleme26f2ALTN  36166  cdleme26f2  36167  cdleme27a  36169  cdleme32b  36244  cdleme32d  36246  cdleme32f  36248  cdleme39n  36268  cdleme40n  36270  cdlemg2fv2  36402  cdlemg17h  36470  cdlemg27b  36498  cdlemg28b  36505  cdlemg28  36506  cdlemg29  36507  cdlemg33a  36508  cdlemg33d  36511  cdlemk7u-2N  36690  cdlemk11u-2N  36691  cdlemk12u-2N  36692  cdlemk26-3  36708  cdlemk27-3  36709  cdlemkfid3N  36727  cdlemn11c  37012