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  17056  axpasch  29552  3atlem4  40746  llncvrlpln2  40817  2lplnja  40879  2lnat  41044  llnexchb2  41129  lhp2lt  41261  lhpmcvr5N  41287  4atexlemq  41311  4atexlemex6  41334  trlval2  41423  cdleme7d  41506  cdleme7e  41507  cdleme7ga  41508  cdleme7  41509  cdleme11l  41529  cdleme11  41530  cdleme14  41533  cdleme15a  41534  cdleme15b  41535  cdleme15  41538  cdleme16b  41539  cdleme16c  41540  cdleme16d  41541  cdleme18d  41555  cdleme19b  41564  cdleme19e  41567  cdleme20d  41572  cdleme20g  41575  cdleme20h  41576  cdleme20i  41577  cdleme20j  41578  cdleme20l2  41581  cdleme20l  41582  cdleme20m  41583  cdleme21d  41590  cdleme21e  41591  cdleme21h  41594  cdleme22f  41606  cdleme23a  41609  cdleme23b  41610  cdleme23c  41611  cdleme24  41612  cdleme25a  41613  cdleme25dN  41616  cdleme26ee  41620  cdleme26fALTN  41622  cdleme26f  41623  cdleme26f2ALTN  41624  cdleme26f2  41625  cdleme27a  41627  cdlemefr29bpre0N  41666  cdlemefr29clN  41667  cdlemefr32fvaN  41669  cdlemefr32fva1  41670  cdleme41sn3a  41693  cdleme35a  41708  cdleme35fnpq  41709  cdleme35b  41710  cdleme35c  41711  cdleme35d  41712  cdleme35f  41714  cdleme36m  41721  cdleme37m  41722  cdleme39n  41726  cdleme43bN  41750  cdleme43dN  41752  cdleme17d2  41755  cdlemeg46c  41773  cdlemeg46nlpq  41777  cdlemeg46ngfr  41778  cdlemeg46req  41789  cdlemeg46gfv  41790  cdleme50trn1  41809  cdleme50trn2a  41810  cdlemf1  41821  cdlemf  41823  cdlemg10a  41900  cdlemg10  41901  cdlemg12d  41906  cdlemg12e  41907  cdlemg12f  41908  cdlemg12g  41909  cdlemg12  41910  cdlemg13  41912  cdlemg16ALTN  41918  cdlemg17b  41922  cdlemg17h  41928  cdlemg17pq  41932  cdlemg17iqN  41934  cdlemg17  41937  cdlemg19a  41943  cdlemg19  41944  cdlemg21  41946  cdlemg27a  41952  cdlemg27b  41956  cdlemg31c  41959  cdlemg33b0  41961  cdlemg33a  41966  cdlemg48  41997  tendocan  42084  cdlemk26-3  42166  cdlemk27-3  42167  cdlemk28-3  42168  cdlemk37  42174  cdlemky  42186  cdlemkyu  42187  cdlemk11ta  42189  cdlemkid3N  42193  cdlemk42  42201  cdlemk42yN  42204  cdlemk11t  42206  cdlemk45  42207  cdlemk46  42208  cdlemk47  42209  cdlemk51  42213  cdlemk52  42214  cdlemk53a  42215  cdleml4N  42239  dihord2pre2  42486  dihord4  42518  dihord5apre  42522  dihmeetlem1N  42550  dihmeetlem15N  42581  mapdpglem32  42965  mzpcong  44183  mullimc  46843  mullimcf  46850  addlimc  46873  iscnrm3rlem8  50276