Theorem simp12l 1288

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

Assertion

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

Proof of Theorem simp12l

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

Syntax hints:   → wi 4   ∧ wa 395   ∧ 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 207  df-an 396  df-3an 1089

This theorem is referenced by:  ackbij1lem16  10156  axcontlem4  29036  eqlkr  39545  athgt  39902  llncvrlpln2  40003  4atlem11b  40054  2lnat  40230  cdlemblem  40239  pclfinN  40346  lhp2lt  40447  lhpmcvr5N  40473  lhpmcvr6N  40474  lhp2at0  40478  lhp2atnle  40479  lhp2at0nle  40481  4atexlemex6  40520  cdlemd2  40645  cdlemd7  40650  cdlemd8  40651  cdlemd9  40652  cdleme7aa  40688  cdleme7c  40691  cdleme7d  40692  cdleme7e  40693  cdleme7ga  40694  cdleme7  40695  cdleme11c  40707  cdleme11dN  40708  cdleme11e  40709  cdleme11  40716  cdleme14  40719  cdleme15a  40720  cdleme15b  40721  cdleme15d  40723  cdleme15  40724  cdleme16b  40725  cdleme16c  40726  cdleme16d  40727  cdleme18d  40741  cdleme19b  40750  cdleme19e  40753  cdleme20d  40758  cdleme20g  40761  cdleme20h  40762  cdleme20i  40763  cdleme20j  40764  cdleme20l2  40767  cdleme20l  40768  cdleme20m  40769  cdleme21c  40773  cdleme21ct  40775  cdleme21d  40776  cdleme21e  40777  cdleme22cN  40788  cdleme22f  40792  cdleme22f2  40793  cdleme23a  40795  cdleme23b  40796  cdleme23c  40797  cdleme25a  40799  cdleme25dN  40802  cdleme26fALTN  40808  cdleme26f  40809  cdleme26f2ALTN  40810  cdleme26f2  40811  cdlemefr29bpre0N  40852  cdlemefr29clN  40853  cdlemefr32fvaN  40855  cdlemefr32fva1  40856  cdleme41sn3a  40879  cdleme32le  40893  cdleme35a  40894  cdleme35fnpq  40895  cdleme35b  40896  cdleme35c  40897  cdleme35d  40898  cdleme35e  40899  cdleme35f  40900  cdleme36a  40906  cdleme37m  40908  cdleme39n  40912  cdleme43bN  40936  cdleme43dN  40938  cdleme17d2  40941  cdlemeg46c  40959  cdlemeg46nlpq  40963  cdlemeg46ngfr  40964  cdlemeg46req  40975  cdlemeg46gfv  40976  cdleme50trn1  40995  cdleme50trn2a  40996  cdlemf1  41007  trlord  41015  cdlemb3  41052  cdlemg7fvbwN  41053  cdlemg7aN  41071  cdlemg10a  41086  cdlemg10  41087  cdlemg12d  41092  cdlemg12e  41093  cdlemg12f  41094  cdlemg12g  41095  cdlemg12  41096  cdlemg13a  41097  cdlemg13  41098  cdlemg17b  41108  cdlemg17f  41112  cdlemg17g  41113  cdlemg17h  41114  cdlemg17pq  41118  cdlemg17  41123  cdlemg19a  41129  cdlemg19  41130  cdlemg21  41132  cdlemg27a  41138  cdlemg27b  41142  cdlemg31c  41145  cdlemg33b0  41147  cdlemg33a  41152  trlcone  41174  cdlemg44  41179  cdlemg48  41183  cdlemk37  41360  cdlemky  41372  cdlemk11ta  41375  cdleml4N  41425  dihord1  41664  dihord2pre2  41672  dihord4  41704  dihord5apre  41708  dihmeetlem1N  41736  dihglblem3N  41741  dihglbcpreN  41746  dihmeetlem3N  41751  dihmeetlem13N  41765  mapdpglem32  42151  baerlem3lem2  42156  baerlem5alem2  42157  baerlem5blem2  42158  mzpcong  43400  iscnrm3rlem8  49422