Theorem simp23l 1293

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

Assertion

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

Proof of Theorem simp23l

Step	Hyp	Ref	Expression
1		simp3l 1200	. 2 ⊢ ((𝜒 ∧ 𝜃 ∧ (𝜑 ∧ 𝜓)) → 𝜑)
2	1	3ad2ant2 1133	1 ⊢ ((𝜏 ∧ (𝜒 ∧ 𝜃 ∧ (𝜑 ∧ 𝜓)) ∧ 𝜂) → 𝜑)

Syntax hints:   → wi 4   ∧ wa 396   ∧ w3a 1086

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 206  df-an 397  df-3an 1088

This theorem is referenced by:  ax5seglem6  27410  lshpkrlem5  37340  lplnexllnN  37790  4atexlemt  38279  4atex2  38303  4atex3  38307  trlval4  38414  cdlemc5  38421  cdlemc6  38422  cdlemd2  38425  cdleme0e  38443  cdleme0moN  38451  cdleme3g  38460  cdleme3h  38461  cdleme3  38463  cdleme4  38464  cdleme5  38466  cdleme9  38479  cdleme11fN  38490  cdleme11j  38493  cdleme11k  38494  cdleme11l  38495  cdleme11  38496  cdleme14  38499  cdleme15a  38500  cdleme15b  38501  cdleme15c  38502  cdleme16b  38505  cdleme16c  38506  cdleme16d  38507  cdleme16e  38508  cdleme16f  38509  cdleme17d1  38515  cdleme18c  38519  cdlemednpq  38525  cdleme19c  38531  cdleme20bN  38536  cdleme20d  38538  cdleme20f  38540  cdleme20g  38541  cdleme20h  38542  cdleme20j  38544  cdleme20l2  38547  cdleme20l  38548  cdleme20m  38549  cdleme22cN  38568  cdleme22d  38569  cdleme22e  38570  cdleme22f  38572  cdleme26fALTN  38588  cdleme26f  38589  cdleme26f2ALTN  38590  cdleme26f2  38591  cdleme27a  38593  cdleme28a  38596  cdlemefs44  38652  cdlemefs45ee  38656  cdleme32b  38668  cdleme32c  38669  cdleme32e  38671  cdleme35sn2aw  38684  cdleme37m  38688  cdleme39n  38692  cdleme40n  38694  cdleme40w  38696  cdleme42k  38710  cdlemeg47rv2  38736  cdlemeg46rjgN  38748  cdlemeg46rgv  38754  cdlemeg46req  38755  cdlemg2fv2  38826  cdlemg17h  38894  cdlemg31b0a  38921  cdlemg27b  38922  cdlemg31d  38926  cdlemg28b  38929  cdlemg28  38930  cdlemg29  38931  cdlemg33a  38932  cdlemg33b  38933  cdlemg33c  38934  cdlemg33d  38935  cdlemg33e  38936  cdlemg44a  38957  cdlemk7u-2N  39114  cdlemk11u-2N  39115  cdlemk12u-2N  39116  cdlemk26-3  39132  cdlemk27-3  39133  cdlemkfid3N  39151  cdlemn2  39421  cdlemn10  39432  cdlemn11c  39435