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  29052  eqlkr  39469  athgt  39826  llncvrlpln2  39927  4atlem11b  39978  2lnat  40154  cdlemblem  40163  pclfinN  40270  lhp2lt  40371  lhpmcvr5N  40397  lhpmcvr6N  40398  lhp2at0  40402  lhp2atnle  40403  lhp2at0nle  40405  4atexlemex6  40444  cdlemd2  40569  cdlemd7  40574  cdlemd8  40575  cdlemd9  40576  cdleme7aa  40612  cdleme7c  40615  cdleme7d  40616  cdleme7e  40617  cdleme7ga  40618  cdleme7  40619  cdleme11c  40631  cdleme11dN  40632  cdleme11e  40633  cdleme11  40640  cdleme14  40643  cdleme15a  40644  cdleme15b  40645  cdleme15d  40647  cdleme15  40648  cdleme16b  40649  cdleme16c  40650  cdleme16d  40651  cdleme18d  40665  cdleme19b  40674  cdleme19e  40677  cdleme20d  40682  cdleme20g  40685  cdleme20h  40686  cdleme20i  40687  cdleme20j  40688  cdleme20l2  40691  cdleme20l  40692  cdleme20m  40693  cdleme21c  40697  cdleme21ct  40699  cdleme21d  40700  cdleme21e  40701  cdleme22cN  40712  cdleme22f  40716  cdleme22f2  40717  cdleme23a  40719  cdleme23b  40720  cdleme23c  40721  cdleme25a  40723  cdleme25dN  40726  cdleme26fALTN  40732  cdleme26f  40733  cdleme26f2ALTN  40734  cdleme26f2  40735  cdlemefr29bpre0N  40776  cdlemefr29clN  40777  cdlemefr32fvaN  40779  cdlemefr32fva1  40780  cdleme41sn3a  40803  cdleme32le  40817  cdleme35a  40818  cdleme35fnpq  40819  cdleme35b  40820  cdleme35c  40821  cdleme35d  40822  cdleme35e  40823  cdleme35f  40824  cdleme36a  40830  cdleme37m  40832  cdleme39n  40836  cdleme43bN  40860  cdleme43dN  40862  cdleme17d2  40865  cdlemeg46c  40883  cdlemeg46nlpq  40887  cdlemeg46ngfr  40888  cdlemeg46req  40899  cdlemeg46gfv  40900  cdleme50trn1  40919  cdleme50trn2a  40920  cdlemf1  40931  trlord  40939  cdlemb3  40976  cdlemg7fvbwN  40977  cdlemg7aN  40995  cdlemg10a  41010  cdlemg10  41011  cdlemg12d  41016  cdlemg12e  41017  cdlemg12f  41018  cdlemg12g  41019  cdlemg12  41020  cdlemg13a  41021  cdlemg13  41022  cdlemg17b  41032  cdlemg17f  41036  cdlemg17g  41037  cdlemg17h  41038  cdlemg17pq  41042  cdlemg17  41047  cdlemg19a  41053  cdlemg19  41054  cdlemg21  41056  cdlemg27a  41062  cdlemg27b  41066  cdlemg31c  41069  cdlemg33b0  41071  cdlemg33a  41076  trlcone  41098  cdlemg44  41103  cdlemg48  41107  cdlemk37  41284  cdlemky  41296  cdlemk11ta  41299  cdleml4N  41349  dihord1  41588  dihord2pre2  41596  dihord4  41628  dihord5apre  41632  dihmeetlem1N  41660  dihglblem3N  41665  dihglbcpreN  41670  dihmeetlem3N  41675  dihmeetlem13N  41689  mapdpglem32  42075  baerlem3lem2  42080  baerlem5alem2  42081  baerlem5blem2  42082  mzpcong  43323  iscnrm3rlem8  49300