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 1133	1 ⊢ (((𝜒 ∧ 𝜃 ∧ (𝜑 ∧ 𝜓)) ∧ 𝜏 ∧ 𝜂) → 𝜑)

Syntax hints:   → wi 4   ∧ wa 395   ∧ 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 207  df-an 396  df-3an 1088

This theorem is referenced by:  pceu  16776  axpasch  28904  3atlem4  39465  llncvrlpln2  39536  2lplnja  39598  2lnat  39763  llnexchb2  39848  lhp2lt  39980  lhpmcvr5N  40006  4atexlemq  40030  4atexlemex6  40053  trlval2  40142  cdleme7d  40225  cdleme7e  40226  cdleme7ga  40227  cdleme7  40228  cdleme11l  40248  cdleme11  40249  cdleme14  40252  cdleme15a  40253  cdleme15b  40254  cdleme15  40257  cdleme16b  40258  cdleme16c  40259  cdleme16d  40260  cdleme18d  40274  cdleme19b  40283  cdleme19e  40286  cdleme20d  40291  cdleme20g  40294  cdleme20h  40295  cdleme20i  40296  cdleme20j  40297  cdleme20l2  40300  cdleme20l  40301  cdleme20m  40302  cdleme21d  40309  cdleme21e  40310  cdleme21h  40313  cdleme22f  40325  cdleme23a  40328  cdleme23b  40329  cdleme23c  40330  cdleme24  40331  cdleme25a  40332  cdleme25dN  40335  cdleme26ee  40339  cdleme26fALTN  40341  cdleme26f  40342  cdleme26f2ALTN  40343  cdleme26f2  40344  cdleme27a  40346  cdlemefr29bpre0N  40385  cdlemefr29clN  40386  cdlemefr32fvaN  40388  cdlemefr32fva1  40389  cdleme41sn3a  40412  cdleme35a  40427  cdleme35fnpq  40428  cdleme35b  40429  cdleme35c  40430  cdleme35d  40431  cdleme35f  40433  cdleme36m  40440  cdleme37m  40441  cdleme39n  40445  cdleme43bN  40469  cdleme43dN  40471  cdleme17d2  40474  cdlemeg46c  40492  cdlemeg46nlpq  40496  cdlemeg46ngfr  40497  cdlemeg46req  40508  cdlemeg46gfv  40509  cdleme50trn1  40528  cdleme50trn2a  40529  cdlemf1  40540  cdlemf  40542  cdlemg10a  40619  cdlemg10  40620  cdlemg12d  40625  cdlemg12e  40626  cdlemg12f  40627  cdlemg12g  40628  cdlemg12  40629  cdlemg13  40631  cdlemg16ALTN  40637  cdlemg17b  40641  cdlemg17h  40647  cdlemg17pq  40651  cdlemg17iqN  40653  cdlemg17  40656  cdlemg19a  40662  cdlemg19  40663  cdlemg21  40665  cdlemg27a  40671  cdlemg27b  40675  cdlemg31c  40678  cdlemg33b0  40680  cdlemg33a  40685  cdlemg48  40716  tendocan  40803  cdlemk26-3  40885  cdlemk27-3  40886  cdlemk28-3  40887  cdlemk37  40893  cdlemky  40905  cdlemkyu  40906  cdlemk11ta  40908  cdlemkid3N  40912  cdlemk42  40920  cdlemk42yN  40923  cdlemk11t  40925  cdlemk45  40926  cdlemk46  40927  cdlemk47  40928  cdlemk51  40932  cdlemk52  40933  cdlemk53a  40934  cdleml4N  40958  dihord2pre2  41205  dihord4  41237  dihord5apre  41241  dihmeetlem1N  41269  dihmeetlem15N  41300  mapdpglem32  41684  mzpcong  42945  mullimc  45598  mullimcf  45605  addlimc  45630  iscnrm3rlem8  48932