Theorem simp12l 1287

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

Assertion

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

Proof of Theorem simp12l

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

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

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 1088

This theorem is referenced by:  ackbij1lem16  10132  axcontlem4  28947  eqlkr  39218  athgt  39575  llncvrlpln2  39676  4atlem11b  39727  2lnat  39903  cdlemblem  39912  pclfinN  40019  lhp2lt  40120  lhpmcvr5N  40146  lhpmcvr6N  40147  lhp2at0  40151  lhp2atnle  40152  lhp2at0nle  40154  4atexlemex6  40193  cdlemd2  40318  cdlemd7  40323  cdlemd8  40324  cdlemd9  40325  cdleme7aa  40361  cdleme7c  40364  cdleme7d  40365  cdleme7e  40366  cdleme7ga  40367  cdleme7  40368  cdleme11c  40380  cdleme11dN  40381  cdleme11e  40382  cdleme11  40389  cdleme14  40392  cdleme15a  40393  cdleme15b  40394  cdleme15d  40396  cdleme15  40397  cdleme16b  40398  cdleme16c  40399  cdleme16d  40400  cdleme18d  40414  cdleme19b  40423  cdleme19e  40426  cdleme20d  40431  cdleme20g  40434  cdleme20h  40435  cdleme20i  40436  cdleme20j  40437  cdleme20l2  40440  cdleme20l  40441  cdleme20m  40442  cdleme21c  40446  cdleme21ct  40448  cdleme21d  40449  cdleme21e  40450  cdleme22cN  40461  cdleme22f  40465  cdleme22f2  40466  cdleme23a  40468  cdleme23b  40469  cdleme23c  40470  cdleme25a  40472  cdleme25dN  40475  cdleme26fALTN  40481  cdleme26f  40482  cdleme26f2ALTN  40483  cdleme26f2  40484  cdlemefr29bpre0N  40525  cdlemefr29clN  40526  cdlemefr32fvaN  40528  cdlemefr32fva1  40529  cdleme41sn3a  40552  cdleme32le  40566  cdleme35a  40567  cdleme35fnpq  40568  cdleme35b  40569  cdleme35c  40570  cdleme35d  40571  cdleme35e  40572  cdleme35f  40573  cdleme36a  40579  cdleme37m  40581  cdleme39n  40585  cdleme43bN  40609  cdleme43dN  40611  cdleme17d2  40614  cdlemeg46c  40632  cdlemeg46nlpq  40636  cdlemeg46ngfr  40637  cdlemeg46req  40648  cdlemeg46gfv  40649  cdleme50trn1  40668  cdleme50trn2a  40669  cdlemf1  40680  trlord  40688  cdlemb3  40725  cdlemg7fvbwN  40726  cdlemg7aN  40744  cdlemg10a  40759  cdlemg10  40760  cdlemg12d  40765  cdlemg12e  40766  cdlemg12f  40767  cdlemg12g  40768  cdlemg12  40769  cdlemg13a  40770  cdlemg13  40771  cdlemg17b  40781  cdlemg17f  40785  cdlemg17g  40786  cdlemg17h  40787  cdlemg17pq  40791  cdlemg17  40796  cdlemg19a  40802  cdlemg19  40803  cdlemg21  40805  cdlemg27a  40811  cdlemg27b  40815  cdlemg31c  40818  cdlemg33b0  40820  cdlemg33a  40825  trlcone  40847  cdlemg44  40852  cdlemg48  40856  cdlemk37  41033  cdlemky  41045  cdlemk11ta  41048  cdleml4N  41098  dihord1  41337  dihord2pre2  41345  dihord4  41377  dihord5apre  41381  dihmeetlem1N  41409  dihglblem3N  41414  dihglbcpreN  41419  dihmeetlem3N  41424  dihmeetlem13N  41438  mapdpglem32  41824  baerlem3lem2  41829  baerlem5alem2  41830  baerlem5blem2  41831  mzpcong  43089  iscnrm3rlem8  49071