Theorem simp13l 1288

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

Assertion

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

Proof of Theorem simp13l

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

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

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 1089

This theorem is referenced by:  pceu  16729  axpasch  27953  3atlem4  38022  llncvrlpln2  38093  2lplnja  38155  2lnat  38320  llnexchb2  38405  lhp2lt  38537  lhpmcvr5N  38563  4atexlemq  38587  4atexlemex6  38610  trlval2  38699  cdleme7d  38782  cdleme7e  38783  cdleme7ga  38784  cdleme7  38785  cdleme11l  38805  cdleme11  38806  cdleme14  38809  cdleme15a  38810  cdleme15b  38811  cdleme15  38814  cdleme16b  38815  cdleme16c  38816  cdleme16d  38817  cdleme18d  38831  cdleme19b  38840  cdleme19e  38843  cdleme20d  38848  cdleme20g  38851  cdleme20h  38852  cdleme20i  38853  cdleme20j  38854  cdleme20l2  38857  cdleme20l  38858  cdleme20m  38859  cdleme21d  38866  cdleme21e  38867  cdleme21h  38870  cdleme22f  38882  cdleme23a  38885  cdleme23b  38886  cdleme23c  38887  cdleme24  38888  cdleme25a  38889  cdleme25dN  38892  cdleme26ee  38896  cdleme26fALTN  38898  cdleme26f  38899  cdleme26f2ALTN  38900  cdleme26f2  38901  cdleme27a  38903  cdlemefr29bpre0N  38942  cdlemefr29clN  38943  cdlemefr32fvaN  38945  cdlemefr32fva1  38946  cdleme41sn3a  38969  cdleme35a  38984  cdleme35fnpq  38985  cdleme35b  38986  cdleme35c  38987  cdleme35d  38988  cdleme35f  38990  cdleme36m  38997  cdleme37m  38998  cdleme39n  39002  cdleme43bN  39026  cdleme43dN  39028  cdleme17d2  39031  cdlemeg46c  39049  cdlemeg46nlpq  39053  cdlemeg46ngfr  39054  cdlemeg46req  39065  cdlemeg46gfv  39066  cdleme50trn1  39085  cdleme50trn2a  39086  cdlemf1  39097  cdlemf  39099  cdlemg10a  39176  cdlemg10  39177  cdlemg12d  39182  cdlemg12e  39183  cdlemg12f  39184  cdlemg12g  39185  cdlemg12  39186  cdlemg13  39188  cdlemg16ALTN  39194  cdlemg17b  39198  cdlemg17h  39204  cdlemg17pq  39208  cdlemg17iqN  39210  cdlemg17  39213  cdlemg19a  39219  cdlemg19  39220  cdlemg21  39222  cdlemg27a  39228  cdlemg27b  39232  cdlemg31c  39235  cdlemg33b0  39237  cdlemg33a  39242  cdlemg48  39273  tendocan  39360  cdlemk26-3  39442  cdlemk27-3  39443  cdlemk28-3  39444  cdlemk37  39450  cdlemky  39462  cdlemkyu  39463  cdlemk11ta  39465  cdlemkid3N  39469  cdlemk42  39477  cdlemk42yN  39480  cdlemk11t  39482  cdlemk45  39483  cdlemk46  39484  cdlemk47  39485  cdlemk51  39489  cdlemk52  39490  cdlemk53a  39491  cdleml4N  39515  dihord2pre2  39762  dihord4  39794  dihord5apre  39798  dihmeetlem1N  39826  dihmeetlem15N  39857  mapdpglem32  40241  mzpcong  41354  mullimc  43977  mullimcf  43984  addlimc  44009  iscnrm3rlem8  47100