Theorem simp13l 1289

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

Assertion

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

Proof of Theorem simp13l

Step	Hyp	Ref	Expression
1		simp3l 1202	. 2 ⊢ ((𝜒 ∧ 𝜃 ∧ (𝜑 ∧ 𝜓)) → 𝜑)
2	1	3ad2ant1 1134	1 ⊢ (((𝜒 ∧ 𝜃 ∧ (𝜑 ∧ 𝜓)) ∧ 𝜏 ∧ 𝜂) → 𝜑)

Syntax hints:   → wi 4   ∧ wa 397   ∧ w3a 1088

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 398  df-3an 1090

This theorem is referenced by:  pceu  16779  axpasch  28199  3atlem4  38357  llncvrlpln2  38428  2lplnja  38490  2lnat  38655  llnexchb2  38740  lhp2lt  38872  lhpmcvr5N  38898  4atexlemq  38922  4atexlemex6  38945  trlval2  39034  cdleme7d  39117  cdleme7e  39118  cdleme7ga  39119  cdleme7  39120  cdleme11l  39140  cdleme11  39141  cdleme14  39144  cdleme15a  39145  cdleme15b  39146  cdleme15  39149  cdleme16b  39150  cdleme16c  39151  cdleme16d  39152  cdleme18d  39166  cdleme19b  39175  cdleme19e  39178  cdleme20d  39183  cdleme20g  39186  cdleme20h  39187  cdleme20i  39188  cdleme20j  39189  cdleme20l2  39192  cdleme20l  39193  cdleme20m  39194  cdleme21d  39201  cdleme21e  39202  cdleme21h  39205  cdleme22f  39217  cdleme23a  39220  cdleme23b  39221  cdleme23c  39222  cdleme24  39223  cdleme25a  39224  cdleme25dN  39227  cdleme26ee  39231  cdleme26fALTN  39233  cdleme26f  39234  cdleme26f2ALTN  39235  cdleme26f2  39236  cdleme27a  39238  cdlemefr29bpre0N  39277  cdlemefr29clN  39278  cdlemefr32fvaN  39280  cdlemefr32fva1  39281  cdleme41sn3a  39304  cdleme35a  39319  cdleme35fnpq  39320  cdleme35b  39321  cdleme35c  39322  cdleme35d  39323  cdleme35f  39325  cdleme36m  39332  cdleme37m  39333  cdleme39n  39337  cdleme43bN  39361  cdleme43dN  39363  cdleme17d2  39366  cdlemeg46c  39384  cdlemeg46nlpq  39388  cdlemeg46ngfr  39389  cdlemeg46req  39400  cdlemeg46gfv  39401  cdleme50trn1  39420  cdleme50trn2a  39421  cdlemf1  39432  cdlemf  39434  cdlemg10a  39511  cdlemg10  39512  cdlemg12d  39517  cdlemg12e  39518  cdlemg12f  39519  cdlemg12g  39520  cdlemg12  39521  cdlemg13  39523  cdlemg16ALTN  39529  cdlemg17b  39533  cdlemg17h  39539  cdlemg17pq  39543  cdlemg17iqN  39545  cdlemg17  39548  cdlemg19a  39554  cdlemg19  39555  cdlemg21  39557  cdlemg27a  39563  cdlemg27b  39567  cdlemg31c  39570  cdlemg33b0  39572  cdlemg33a  39577  cdlemg48  39608  tendocan  39695  cdlemk26-3  39777  cdlemk27-3  39778  cdlemk28-3  39779  cdlemk37  39785  cdlemky  39797  cdlemkyu  39798  cdlemk11ta  39800  cdlemkid3N  39804  cdlemk42  39812  cdlemk42yN  39815  cdlemk11t  39817  cdlemk45  39818  cdlemk46  39819  cdlemk47  39820  cdlemk51  39824  cdlemk52  39825  cdlemk53a  39826  cdleml4N  39850  dihord2pre2  40097  dihord4  40129  dihord5apre  40133  dihmeetlem1N  40161  dihmeetlem15N  40192  mapdpglem32  40576  mzpcong  41711  mullimc  44332  mullimcf  44339  addlimc  44364  iscnrm3rlem8  47580