Theorem simp12l 1174

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

Assertion

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

Proof of Theorem simp12l

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

Syntax hints:   → wi 4   ∧ wa 384   ∧ w3a 1037

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 197  df-an 386  df-3an 1039

This theorem is referenced by:  ackbij1lem16  9057  axcontlem4  25847  eqlkr  34386  athgt  34742  llncvrlpln2  34843  4atlem11b  34894  2lnat  35070  cdlemblem  35079  pclfinN  35186  lhp2lt  35287  lhpmcvr5N  35313  lhpmcvr6N  35314  lhp2at0  35318  lhp2atnle  35319  lhp2at0nle  35321  4atexlemex6  35360  cdlemd2  35486  cdlemd7  35491  cdlemd8  35492  cdlemd9  35493  cdleme7aa  35529  cdleme7c  35532  cdleme7d  35533  cdleme7e  35534  cdleme7ga  35535  cdleme7  35536  cdleme11c  35548  cdleme11dN  35549  cdleme11e  35550  cdleme11  35557  cdleme14  35560  cdleme15a  35561  cdleme15b  35562  cdleme15d  35564  cdleme15  35565  cdleme16b  35566  cdleme16c  35567  cdleme16d  35568  cdleme18d  35582  cdleme19b  35592  cdleme19e  35595  cdleme20d  35600  cdleme20g  35603  cdleme20h  35604  cdleme20i  35605  cdleme20j  35606  cdleme20l2  35609  cdleme20l  35610  cdleme20m  35611  cdleme21c  35615  cdleme21ct  35617  cdleme21d  35618  cdleme21e  35619  cdleme22cN  35630  cdleme22f  35634  cdleme22f2  35635  cdleme23a  35637  cdleme23b  35638  cdleme23c  35639  cdleme25a  35641  cdleme25dN  35644  cdleme26fALTN  35650  cdleme26f  35651  cdleme26f2ALTN  35652  cdleme26f2  35653  cdlemefr29bpre0N  35694  cdlemefr29clN  35695  cdlemefr32fvaN  35697  cdlemefr32fva1  35698  cdleme41sn3a  35721  cdleme32le  35735  cdleme35a  35736  cdleme35fnpq  35737  cdleme35b  35738  cdleme35c  35739  cdleme35d  35740  cdleme35e  35741  cdleme35f  35742  cdleme36a  35748  cdleme37m  35750  cdleme39n  35754  cdleme43bN  35778  cdleme43dN  35780  cdleme17d2  35783  cdlemeg46c  35801  cdlemeg46nlpq  35805  cdlemeg46ngfr  35806  cdlemeg46req  35817  cdlemeg46gfv  35818  cdleme50trn1  35837  cdleme50trn2a  35838  cdlemf1  35849  trlord  35857  cdlemb3  35894  cdlemg7fvbwN  35895  cdlemg7aN  35913  cdlemg10a  35928  cdlemg10  35929  cdlemg12d  35934  cdlemg12e  35935  cdlemg12f  35936  cdlemg12g  35937  cdlemg12  35938  cdlemg13a  35939  cdlemg13  35940  cdlemg17b  35950  cdlemg17f  35954  cdlemg17g  35955  cdlemg17h  35956  cdlemg17pq  35960  cdlemg17  35965  cdlemg19a  35971  cdlemg19  35972  cdlemg21  35974  cdlemg27a  35980  cdlemg27b  35984  cdlemg31c  35987  cdlemg33b0  35989  cdlemg33a  35994  trlcone  36016  cdlemg44  36021  cdlemg48  36025  cdlemk37  36202  cdlemky  36214  cdlemk11ta  36217  cdleml4N  36267  dihord1  36507  dihord2pre2  36515  dihord4  36547  dihord5apre  36551  dihmeetlem1N  36579  dihglblem3N  36584  dihglbcpreN  36589  dihmeetlem3N  36594  dihmeetlem13N  36608  mapdpglem32  36994  baerlem3lem2  36999  baerlem5alem2  37000  baerlem5blem2  37001  mzpcong  37539