Theorem simp12l 1305

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

Assertion

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

Proof of Theorem simp12l

Step	Hyp	Ref	Expression
1		simp2l 1218	. 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:  ackbij1lem16  10293  axcontlem4  29527  eqlkr  40124  athgt  40481  llncvrlpln2  40582  4atlem11b  40633  2lnat  40809  cdlemblem  40818  pclfinN  40925  lhp2lt  41026  lhpmcvr5N  41052  lhpmcvr6N  41053  lhp2at0  41057  lhp2atnle  41058  lhp2at0nle  41060  4atexlemex6  41099  cdlemd2  41224  cdlemd7  41229  cdlemd8  41230  cdlemd9  41231  cdleme7aa  41267  cdleme7c  41270  cdleme7d  41271  cdleme7e  41272  cdleme7ga  41273  cdleme7  41274  cdleme11c  41286  cdleme11dN  41287  cdleme11e  41288  cdleme11  41295  cdleme14  41298  cdleme15a  41299  cdleme15b  41300  cdleme15d  41302  cdleme15  41303  cdleme16b  41304  cdleme16c  41305  cdleme16d  41306  cdleme18d  41320  cdleme19b  41329  cdleme19e  41332  cdleme20d  41337  cdleme20g  41340  cdleme20h  41341  cdleme20i  41342  cdleme20j  41343  cdleme20l2  41346  cdleme20l  41347  cdleme20m  41348  cdleme21c  41352  cdleme21ct  41354  cdleme21d  41355  cdleme21e  41356  cdleme22cN  41367  cdleme22f  41371  cdleme22f2  41372  cdleme23a  41374  cdleme23b  41375  cdleme23c  41376  cdleme25a  41378  cdleme25dN  41381  cdleme26fALTN  41387  cdleme26f  41388  cdleme26f2ALTN  41389  cdleme26f2  41390  cdlemefr29bpre0N  41431  cdlemefr29clN  41432  cdlemefr32fvaN  41434  cdlemefr32fva1  41435  cdleme41sn3a  41458  cdleme32le  41472  cdleme35a  41473  cdleme35fnpq  41474  cdleme35b  41475  cdleme35c  41476  cdleme35d  41477  cdleme35e  41478  cdleme35f  41479  cdleme36a  41485  cdleme37m  41487  cdleme39n  41491  cdleme43bN  41515  cdleme43dN  41517  cdleme17d2  41520  cdlemeg46c  41538  cdlemeg46nlpq  41542  cdlemeg46ngfr  41543  cdlemeg46req  41554  cdlemeg46gfv  41555  cdleme50trn1  41574  cdleme50trn2a  41575  cdlemf1  41586  trlord  41594  cdlemb3  41631  cdlemg7fvbwN  41632  cdlemg7aN  41650  cdlemg10a  41665  cdlemg10  41666  cdlemg12d  41671  cdlemg12e  41672  cdlemg12f  41673  cdlemg12g  41674  cdlemg12  41675  cdlemg13a  41676  cdlemg13  41677  cdlemg17b  41687  cdlemg17f  41691  cdlemg17g  41692  cdlemg17h  41693  cdlemg17pq  41697  cdlemg17  41702  cdlemg19a  41708  cdlemg19  41709  cdlemg21  41711  cdlemg27a  41717  cdlemg27b  41721  cdlemg31c  41724  cdlemg33b0  41726  cdlemg33a  41731  trlcone  41753  cdlemg44  41758  cdlemg48  41762  cdlemk37  41939  cdlemky  41951  cdlemk11ta  41954  cdleml4N  42004  dihord1  42243  dihord2pre2  42251  dihord4  42283  dihord5apre  42287  dihmeetlem1N  42315  dihglblem3N  42320  dihglbcpreN  42325  dihmeetlem3N  42330  dihmeetlem13N  42344  mapdpglem32  42730  baerlem3lem2  42735  baerlem5alem2  42736  baerlem5blem2  42737  mzpcong  43932  iscnrm3rlem8  49999