Theorem simp13l 1307

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

Assertion

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

Proof of Theorem simp13l

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∧ w3a 1103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105

This theorem is used by:  pceu  16944  axpasch  29406  3atlem4  40367  llncvrlpln2  40438  2lplnja  40500  2lnat  40665  llnexchb2  40750  lhp2lt  40882  lhpmcvr5N  40908  4atexlemq  40932  4atexlemex6  40955  trlval2  41044  cdleme7d  41127  cdleme7e  41128  cdleme7ga  41129  cdleme7  41130  cdleme11l  41150  cdleme11  41151  cdleme14  41154  cdleme15a  41155  cdleme15b  41156  cdleme15  41159  cdleme16b  41160  cdleme16c  41161  cdleme16d  41162  cdleme18d  41176  cdleme19b  41185  cdleme19e  41188  cdleme20d  41193  cdleme20g  41196  cdleme20h  41197  cdleme20i  41198  cdleme20j  41199  cdleme20l2  41202  cdleme20l  41203  cdleme20m  41204  cdleme21d  41211  cdleme21e  41212  cdleme21h  41215  cdleme22f  41227  cdleme23a  41230  cdleme23b  41231  cdleme23c  41232  cdleme24  41233  cdleme25a  41234  cdleme25dN  41237  cdleme26ee  41241  cdleme26fALTN  41243  cdleme26f  41244  cdleme26f2ALTN  41245  cdleme26f2  41246  cdleme27a  41248  cdlemefr29bpre0N  41287  cdlemefr29clN  41288  cdlemefr32fvaN  41290  cdlemefr32fva1  41291  cdleme41sn3a  41314  cdleme35a  41329  cdleme35fnpq  41330  cdleme35b  41331  cdleme35c  41332  cdleme35d  41333  cdleme35f  41335  cdleme36m  41342  cdleme37m  41343  cdleme39n  41347  cdleme43bN  41371  cdleme43dN  41373  cdleme17d2  41376  cdlemeg46c  41394  cdlemeg46nlpq  41398  cdlemeg46ngfr  41399  cdlemeg46req  41410  cdlemeg46gfv  41411  cdleme50trn1  41430  cdleme50trn2a  41431  cdlemf1  41442  cdlemf  41444  cdlemg10a  41521  cdlemg10  41522  cdlemg12d  41527  cdlemg12e  41528  cdlemg12f  41529  cdlemg12g  41530  cdlemg12  41531  cdlemg13  41533  cdlemg16ALTN  41539  cdlemg17b  41543  cdlemg17h  41549  cdlemg17pq  41553  cdlemg17iqN  41555  cdlemg17  41558  cdlemg19a  41564  cdlemg19  41565  cdlemg21  41567  cdlemg27a  41573  cdlemg27b  41577  cdlemg31c  41580  cdlemg33b0  41582  cdlemg33a  41587  cdlemg48  41618  tendocan  41705  cdlemk26-3  41787  cdlemk27-3  41788  cdlemk28-3  41789  cdlemk37  41795  cdlemky  41807  cdlemkyu  41808  cdlemk11ta  41810  cdlemkid3N  41814  cdlemk42  41822  cdlemk42yN  41825  cdlemk11t  41827  cdlemk45  41828  cdlemk46  41829  cdlemk47  41830  cdlemk51  41834  cdlemk52  41835  cdlemk53a  41836  cdleml4N  41860  dihord2pre2  42107  dihord4  42139  dihord5apre  42143  dihmeetlem1N  42171  dihmeetlem15N  42202  mapdpglem32  42586  mzpcong  43821  mullimc  46454  mullimcf  46461  addlimc  46484  iscnrm3rlem8  49881