Theorem simp13l 1305

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

Assertion

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

Proof of Theorem simp13l

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

Syntax hints:   → wi 4   ∧ wa 400   ∧ w3a 1101

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 210  df-an 401  df-3an 1103

This theorem is referenced by:  pceu  16896  axpasch  29200  3atlem4  40122  llncvrlpln2  40193  2lplnja  40255  2lnat  40420  llnexchb2  40505  lhp2lt  40637  lhpmcvr5N  40663  4atexlemq  40687  4atexlemex6  40710  trlval2  40799  cdleme7d  40882  cdleme7e  40883  cdleme7ga  40884  cdleme7  40885  cdleme11l  40905  cdleme11  40906  cdleme14  40909  cdleme15a  40910  cdleme15b  40911  cdleme15  40914  cdleme16b  40915  cdleme16c  40916  cdleme16d  40917  cdleme18d  40931  cdleme19b  40940  cdleme19e  40943  cdleme20d  40948  cdleme20g  40951  cdleme20h  40952  cdleme20i  40953  cdleme20j  40954  cdleme20l2  40957  cdleme20l  40958  cdleme20m  40959  cdleme21d  40966  cdleme21e  40967  cdleme21h  40970  cdleme22f  40982  cdleme23a  40985  cdleme23b  40986  cdleme23c  40987  cdleme24  40988  cdleme25a  40989  cdleme25dN  40992  cdleme26ee  40996  cdleme26fALTN  40998  cdleme26f  40999  cdleme26f2ALTN  41000  cdleme26f2  41001  cdleme27a  41003  cdlemefr29bpre0N  41042  cdlemefr29clN  41043  cdlemefr32fvaN  41045  cdlemefr32fva1  41046  cdleme41sn3a  41069  cdleme35a  41084  cdleme35fnpq  41085  cdleme35b  41086  cdleme35c  41087  cdleme35d  41088  cdleme35f  41090  cdleme36m  41097  cdleme37m  41098  cdleme39n  41102  cdleme43bN  41126  cdleme43dN  41128  cdleme17d2  41131  cdlemeg46c  41149  cdlemeg46nlpq  41153  cdlemeg46ngfr  41154  cdlemeg46req  41165  cdlemeg46gfv  41166  cdleme50trn1  41185  cdleme50trn2a  41186  cdlemf1  41197  cdlemf  41199  cdlemg10a  41276  cdlemg10  41277  cdlemg12d  41282  cdlemg12e  41283  cdlemg12f  41284  cdlemg12g  41285  cdlemg12  41286  cdlemg13  41288  cdlemg16ALTN  41294  cdlemg17b  41298  cdlemg17h  41304  cdlemg17pq  41308  cdlemg17iqN  41310  cdlemg17  41313  cdlemg19a  41319  cdlemg19  41320  cdlemg21  41322  cdlemg27a  41328  cdlemg27b  41332  cdlemg31c  41335  cdlemg33b0  41337  cdlemg33a  41342  cdlemg48  41373  tendocan  41460  cdlemk26-3  41542  cdlemk27-3  41543  cdlemk28-3  41544  cdlemk37  41550  cdlemky  41562  cdlemkyu  41563  cdlemk11ta  41565  cdlemkid3N  41569  cdlemk42  41577  cdlemk42yN  41580  cdlemk11t  41582  cdlemk45  41583  cdlemk46  41584  cdlemk47  41585  cdlemk51  41589  cdlemk52  41590  cdlemk53a  41591  cdleml4N  41615  dihord2pre2  41862  dihord4  41894  dihord5apre  41898  dihmeetlem1N  41926  dihmeetlem15N  41957  mapdpglem32  42341  mzpcong  43561  mullimc  46190  mullimcf  46197  addlimc  46220  iscnrm3rlem8  49576