Theorem simp12l 1284

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

Assertion

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

Proof of Theorem simp12l

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

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1085

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 396  df-3an 1087

This theorem is referenced by:  ackbij1lem16  9922  axcontlem4  27238  eqlkr  37040  athgt  37397  llncvrlpln2  37498  4atlem11b  37549  2lnat  37725  cdlemblem  37734  pclfinN  37841  lhp2lt  37942  lhpmcvr5N  37968  lhpmcvr6N  37969  lhp2at0  37973  lhp2atnle  37974  lhp2at0nle  37976  4atexlemex6  38015  cdlemd2  38140  cdlemd7  38145  cdlemd8  38146  cdlemd9  38147  cdleme7aa  38183  cdleme7c  38186  cdleme7d  38187  cdleme7e  38188  cdleme7ga  38189  cdleme7  38190  cdleme11c  38202  cdleme11dN  38203  cdleme11e  38204  cdleme11  38211  cdleme14  38214  cdleme15a  38215  cdleme15b  38216  cdleme15d  38218  cdleme15  38219  cdleme16b  38220  cdleme16c  38221  cdleme16d  38222  cdleme18d  38236  cdleme19b  38245  cdleme19e  38248  cdleme20d  38253  cdleme20g  38256  cdleme20h  38257  cdleme20i  38258  cdleme20j  38259  cdleme20l2  38262  cdleme20l  38263  cdleme20m  38264  cdleme21c  38268  cdleme21ct  38270  cdleme21d  38271  cdleme21e  38272  cdleme22cN  38283  cdleme22f  38287  cdleme22f2  38288  cdleme23a  38290  cdleme23b  38291  cdleme23c  38292  cdleme25a  38294  cdleme25dN  38297  cdleme26fALTN  38303  cdleme26f  38304  cdleme26f2ALTN  38305  cdleme26f2  38306  cdlemefr29bpre0N  38347  cdlemefr29clN  38348  cdlemefr32fvaN  38350  cdlemefr32fva1  38351  cdleme41sn3a  38374  cdleme32le  38388  cdleme35a  38389  cdleme35fnpq  38390  cdleme35b  38391  cdleme35c  38392  cdleme35d  38393  cdleme35e  38394  cdleme35f  38395  cdleme36a  38401  cdleme37m  38403  cdleme39n  38407  cdleme43bN  38431  cdleme43dN  38433  cdleme17d2  38436  cdlemeg46c  38454  cdlemeg46nlpq  38458  cdlemeg46ngfr  38459  cdlemeg46req  38470  cdlemeg46gfv  38471  cdleme50trn1  38490  cdleme50trn2a  38491  cdlemf1  38502  trlord  38510  cdlemb3  38547  cdlemg7fvbwN  38548  cdlemg7aN  38566  cdlemg10a  38581  cdlemg10  38582  cdlemg12d  38587  cdlemg12e  38588  cdlemg12f  38589  cdlemg12g  38590  cdlemg12  38591  cdlemg13a  38592  cdlemg13  38593  cdlemg17b  38603  cdlemg17f  38607  cdlemg17g  38608  cdlemg17h  38609  cdlemg17pq  38613  cdlemg17  38618  cdlemg19a  38624  cdlemg19  38625  cdlemg21  38627  cdlemg27a  38633  cdlemg27b  38637  cdlemg31c  38640  cdlemg33b0  38642  cdlemg33a  38647  trlcone  38669  cdlemg44  38674  cdlemg48  38678  cdlemk37  38855  cdlemky  38867  cdlemk11ta  38870  cdleml4N  38920  dihord1  39159  dihord2pre2  39167  dihord4  39199  dihord5apre  39203  dihmeetlem1N  39231  dihglblem3N  39236  dihglbcpreN  39241  dihmeetlem3N  39246  dihmeetlem13N  39260  mapdpglem32  39646  baerlem3lem2  39651  baerlem5alem2  39652  baerlem5blem2  39653  mzpcong  40710  iscnrm3rlem8  46129