Theorem simp13l 1287

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

Assertion

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

Proof of Theorem simp13l

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

Syntax hints:   → wi 4   ∧ wa 396   ∧ w3a 1086

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 206  df-an 397  df-3an 1088

This theorem is referenced by:  pceu  16617  axpasch  27418  3atlem4  37705  llncvrlpln2  37776  2lplnja  37838  2lnat  38003  llnexchb2  38088  lhp2lt  38220  lhpmcvr5N  38246  4atexlemq  38270  4atexlemex6  38293  trlval2  38382  cdleme7d  38465  cdleme7e  38466  cdleme7ga  38467  cdleme7  38468  cdleme11l  38488  cdleme11  38489  cdleme14  38492  cdleme15a  38493  cdleme15b  38494  cdleme15  38497  cdleme16b  38498  cdleme16c  38499  cdleme16d  38500  cdleme18d  38514  cdleme19b  38523  cdleme19e  38526  cdleme20d  38531  cdleme20g  38534  cdleme20h  38535  cdleme20i  38536  cdleme20j  38537  cdleme20l2  38540  cdleme20l  38541  cdleme20m  38542  cdleme21d  38549  cdleme21e  38550  cdleme21h  38553  cdleme22f  38565  cdleme23a  38568  cdleme23b  38569  cdleme23c  38570  cdleme24  38571  cdleme25a  38572  cdleme25dN  38575  cdleme26ee  38579  cdleme26fALTN  38581  cdleme26f  38582  cdleme26f2ALTN  38583  cdleme26f2  38584  cdleme27a  38586  cdlemefr29bpre0N  38625  cdlemefr29clN  38626  cdlemefr32fvaN  38628  cdlemefr32fva1  38629  cdleme41sn3a  38652  cdleme35a  38667  cdleme35fnpq  38668  cdleme35b  38669  cdleme35c  38670  cdleme35d  38671  cdleme35f  38673  cdleme36m  38680  cdleme37m  38681  cdleme39n  38685  cdleme43bN  38709  cdleme43dN  38711  cdleme17d2  38714  cdlemeg46c  38732  cdlemeg46nlpq  38736  cdlemeg46ngfr  38737  cdlemeg46req  38748  cdlemeg46gfv  38749  cdleme50trn1  38768  cdleme50trn2a  38769  cdlemf1  38780  cdlemf  38782  cdlemg10a  38859  cdlemg10  38860  cdlemg12d  38865  cdlemg12e  38866  cdlemg12f  38867  cdlemg12g  38868  cdlemg12  38869  cdlemg13  38871  cdlemg16ALTN  38877  cdlemg17b  38881  cdlemg17h  38887  cdlemg17pq  38891  cdlemg17iqN  38893  cdlemg17  38896  cdlemg19a  38902  cdlemg19  38903  cdlemg21  38905  cdlemg27a  38911  cdlemg27b  38915  cdlemg31c  38918  cdlemg33b0  38920  cdlemg33a  38925  cdlemg48  38956  tendocan  39043  cdlemk26-3  39125  cdlemk27-3  39126  cdlemk28-3  39127  cdlemk37  39133  cdlemky  39145  cdlemkyu  39146  cdlemk11ta  39148  cdlemkid3N  39152  cdlemk42  39160  cdlemk42yN  39163  cdlemk11t  39165  cdlemk45  39166  cdlemk46  39167  cdlemk47  39168  cdlemk51  39172  cdlemk52  39173  cdlemk53a  39174  cdleml4N  39198  dihord2pre2  39445  dihord4  39477  dihord5apre  39481  dihmeetlem1N  39509  dihmeetlem15N  39540  mapdpglem32  39924  mzpcong  40998  mullimc  43394  mullimcf  43401  addlimc  43426  iscnrm3rlem8  46493