Theorem simp13l 1301

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

Assertion

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

Proof of Theorem simp13l

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

Syntax hints:   → wi 4   ∧ wa 399   ∧ w3a 1097

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 400  df-3an 1099

This theorem is referenced by:  pceu  16865  axpasch  29088  3atlem4  40074  llncvrlpln2  40145  2lplnja  40207  2lnat  40372  llnexchb2  40457  lhp2lt  40589  lhpmcvr5N  40615  4atexlemq  40639  4atexlemex6  40662  trlval2  40751  cdleme7d  40834  cdleme7e  40835  cdleme7ga  40836  cdleme7  40837  cdleme11l  40857  cdleme11  40858  cdleme14  40861  cdleme15a  40862  cdleme15b  40863  cdleme15  40866  cdleme16b  40867  cdleme16c  40868  cdleme16d  40869  cdleme18d  40883  cdleme19b  40892  cdleme19e  40895  cdleme20d  40900  cdleme20g  40903  cdleme20h  40904  cdleme20i  40905  cdleme20j  40906  cdleme20l2  40909  cdleme20l  40910  cdleme20m  40911  cdleme21d  40918  cdleme21e  40919  cdleme21h  40922  cdleme22f  40934  cdleme23a  40937  cdleme23b  40938  cdleme23c  40939  cdleme24  40940  cdleme25a  40941  cdleme25dN  40944  cdleme26ee  40948  cdleme26fALTN  40950  cdleme26f  40951  cdleme26f2ALTN  40952  cdleme26f2  40953  cdleme27a  40955  cdlemefr29bpre0N  40994  cdlemefr29clN  40995  cdlemefr32fvaN  40997  cdlemefr32fva1  40998  cdleme41sn3a  41021  cdleme35a  41036  cdleme35fnpq  41037  cdleme35b  41038  cdleme35c  41039  cdleme35d  41040  cdleme35f  41042  cdleme36m  41049  cdleme37m  41050  cdleme39n  41054  cdleme43bN  41078  cdleme43dN  41080  cdleme17d2  41083  cdlemeg46c  41101  cdlemeg46nlpq  41105  cdlemeg46ngfr  41106  cdlemeg46req  41117  cdlemeg46gfv  41118  cdleme50trn1  41137  cdleme50trn2a  41138  cdlemf1  41149  cdlemf  41151  cdlemg10a  41228  cdlemg10  41229  cdlemg12d  41234  cdlemg12e  41235  cdlemg12f  41236  cdlemg12g  41237  cdlemg12  41238  cdlemg13  41240  cdlemg16ALTN  41246  cdlemg17b  41250  cdlemg17h  41256  cdlemg17pq  41260  cdlemg17iqN  41262  cdlemg17  41265  cdlemg19a  41271  cdlemg19  41272  cdlemg21  41274  cdlemg27a  41280  cdlemg27b  41284  cdlemg31c  41287  cdlemg33b0  41289  cdlemg33a  41294  cdlemg48  41325  tendocan  41412  cdlemk26-3  41494  cdlemk27-3  41495  cdlemk28-3  41496  cdlemk37  41502  cdlemky  41514  cdlemkyu  41515  cdlemk11ta  41517  cdlemkid3N  41521  cdlemk42  41529  cdlemk42yN  41532  cdlemk11t  41534  cdlemk45  41535  cdlemk46  41536  cdlemk47  41537  cdlemk51  41541  cdlemk52  41542  cdlemk53a  41543  cdleml4N  41567  dihord2pre2  41814  dihord4  41846  dihord5apre  41850  dihmeetlem1N  41878  dihmeetlem15N  41909  mapdpglem32  42293  mzpcong  43513  mullimc  46156  mullimcf  46163  addlimc  46186  iscnrm3rlem8  49532