Theorem simp13l 1284

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

Assertion

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

Proof of Theorem simp13l

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

Syntax hints:   → wi 4   ∧ wa 398   ∧ w3a 1083

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 209  df-an 399  df-3an 1085

This theorem is referenced by:  pceu  16177  axpasch  26721  3atlem4  36616  llncvrlpln2  36687  2lplnja  36749  2lnat  36914  llnexchb2  36999  lhp2lt  37131  lhpmcvr5N  37157  4atexlemq  37181  4atexlemex6  37204  trlval2  37293  cdleme7d  37376  cdleme7e  37377  cdleme7ga  37378  cdleme7  37379  cdleme11l  37399  cdleme11  37400  cdleme14  37403  cdleme15a  37404  cdleme15b  37405  cdleme15  37408  cdleme16b  37409  cdleme16c  37410  cdleme16d  37411  cdleme18d  37425  cdleme19b  37434  cdleme19e  37437  cdleme20d  37442  cdleme20g  37445  cdleme20h  37446  cdleme20i  37447  cdleme20j  37448  cdleme20l2  37451  cdleme20l  37452  cdleme20m  37453  cdleme21d  37460  cdleme21e  37461  cdleme21h  37464  cdleme22f  37476  cdleme23a  37479  cdleme23b  37480  cdleme23c  37481  cdleme24  37482  cdleme25a  37483  cdleme25dN  37486  cdleme26ee  37490  cdleme26fALTN  37492  cdleme26f  37493  cdleme26f2ALTN  37494  cdleme26f2  37495  cdleme27a  37497  cdlemefr29bpre0N  37536  cdlemefr29clN  37537  cdlemefr32fvaN  37539  cdlemefr32fva1  37540  cdleme41sn3a  37563  cdleme35a  37578  cdleme35fnpq  37579  cdleme35b  37580  cdleme35c  37581  cdleme35d  37582  cdleme35f  37584  cdleme36m  37591  cdleme37m  37592  cdleme39n  37596  cdleme43bN  37620  cdleme43dN  37622  cdleme17d2  37625  cdlemeg46c  37643  cdlemeg46nlpq  37647  cdlemeg46ngfr  37648  cdlemeg46req  37659  cdlemeg46gfv  37660  cdleme50trn1  37679  cdleme50trn2a  37680  cdlemf1  37691  cdlemf  37693  cdlemg10a  37770  cdlemg10  37771  cdlemg12d  37776  cdlemg12e  37777  cdlemg12f  37778  cdlemg12g  37779  cdlemg12  37780  cdlemg13  37782  cdlemg16ALTN  37788  cdlemg17b  37792  cdlemg17h  37798  cdlemg17pq  37802  cdlemg17iqN  37804  cdlemg17  37807  cdlemg19a  37813  cdlemg19  37814  cdlemg21  37816  cdlemg27a  37822  cdlemg27b  37826  cdlemg31c  37829  cdlemg33b0  37831  cdlemg33a  37836  cdlemg48  37867  tendocan  37954  cdlemk26-3  38036  cdlemk27-3  38037  cdlemk28-3  38038  cdlemk37  38044  cdlemky  38056  cdlemkyu  38057  cdlemk11ta  38059  cdlemkid3N  38063  cdlemk42  38071  cdlemk42yN  38074  cdlemk11t  38076  cdlemk45  38077  cdlemk46  38078  cdlemk47  38079  cdlemk51  38083  cdlemk52  38084  cdlemk53a  38085  cdleml4N  38109  dihord2pre2  38356  dihord4  38388  dihord5apre  38392  dihmeetlem1N  38420  dihmeetlem15N  38451  mapdpglem32  38835  mzpcong  39562  mullimc  41889  mullimcf  41896  addlimc  41921