Theorem simp13l 1288

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

Assertion

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

Proof of Theorem simp13l

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

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1087

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 1089

This theorem is referenced by:  pceu  16893  axpasch  28974  3atlem4  39443  llncvrlpln2  39514  2lplnja  39576  2lnat  39741  llnexchb2  39826  lhp2lt  39958  lhpmcvr5N  39984  4atexlemq  40008  4atexlemex6  40031  trlval2  40120  cdleme7d  40203  cdleme7e  40204  cdleme7ga  40205  cdleme7  40206  cdleme11l  40226  cdleme11  40227  cdleme14  40230  cdleme15a  40231  cdleme15b  40232  cdleme15  40235  cdleme16b  40236  cdleme16c  40237  cdleme16d  40238  cdleme18d  40252  cdleme19b  40261  cdleme19e  40264  cdleme20d  40269  cdleme20g  40272  cdleme20h  40273  cdleme20i  40274  cdleme20j  40275  cdleme20l2  40278  cdleme20l  40279  cdleme20m  40280  cdleme21d  40287  cdleme21e  40288  cdleme21h  40291  cdleme22f  40303  cdleme23a  40306  cdleme23b  40307  cdleme23c  40308  cdleme24  40309  cdleme25a  40310  cdleme25dN  40313  cdleme26ee  40317  cdleme26fALTN  40319  cdleme26f  40320  cdleme26f2ALTN  40321  cdleme26f2  40322  cdleme27a  40324  cdlemefr29bpre0N  40363  cdlemefr29clN  40364  cdlemefr32fvaN  40366  cdlemefr32fva1  40367  cdleme41sn3a  40390  cdleme35a  40405  cdleme35fnpq  40406  cdleme35b  40407  cdleme35c  40408  cdleme35d  40409  cdleme35f  40411  cdleme36m  40418  cdleme37m  40419  cdleme39n  40423  cdleme43bN  40447  cdleme43dN  40449  cdleme17d2  40452  cdlemeg46c  40470  cdlemeg46nlpq  40474  cdlemeg46ngfr  40475  cdlemeg46req  40486  cdlemeg46gfv  40487  cdleme50trn1  40506  cdleme50trn2a  40507  cdlemf1  40518  cdlemf  40520  cdlemg10a  40597  cdlemg10  40598  cdlemg12d  40603  cdlemg12e  40604  cdlemg12f  40605  cdlemg12g  40606  cdlemg12  40607  cdlemg13  40609  cdlemg16ALTN  40615  cdlemg17b  40619  cdlemg17h  40625  cdlemg17pq  40629  cdlemg17iqN  40631  cdlemg17  40634  cdlemg19a  40640  cdlemg19  40641  cdlemg21  40643  cdlemg27a  40649  cdlemg27b  40653  cdlemg31c  40656  cdlemg33b0  40658  cdlemg33a  40663  cdlemg48  40694  tendocan  40781  cdlemk26-3  40863  cdlemk27-3  40864  cdlemk28-3  40865  cdlemk37  40871  cdlemky  40883  cdlemkyu  40884  cdlemk11ta  40886  cdlemkid3N  40890  cdlemk42  40898  cdlemk42yN  40901  cdlemk11t  40903  cdlemk45  40904  cdlemk46  40905  cdlemk47  40906  cdlemk51  40910  cdlemk52  40911  cdlemk53a  40912  cdleml4N  40936  dihord2pre2  41183  dihord4  41215  dihord5apre  41219  dihmeetlem1N  41247  dihmeetlem15N  41278  mapdpglem32  41662  mzpcong  42929  mullimc  45537  mullimcf  45544  addlimc  45569  iscnrm3rlem8  48627