Theorem simp12l 1299

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

Assertion

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

Proof of Theorem simp12l

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

Syntax hints:   → wi 4   ∧ wa 399   ∧ w3a 1097

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 209  df-an 400  df-3an 1099

This theorem is referenced by:  ackbij1lem16  10187  axcontlem4  29114  eqlkr  39687  athgt  40044  llncvrlpln2  40145  4atlem11b  40196  2lnat  40372  cdlemblem  40381  pclfinN  40488  lhp2lt  40589  lhpmcvr5N  40615  lhpmcvr6N  40616  lhp2at0  40620  lhp2atnle  40621  lhp2at0nle  40623  4atexlemex6  40662  cdlemd2  40787  cdlemd7  40792  cdlemd8  40793  cdlemd9  40794  cdleme7aa  40830  cdleme7c  40833  cdleme7d  40834  cdleme7e  40835  cdleme7ga  40836  cdleme7  40837  cdleme11c  40849  cdleme11dN  40850  cdleme11e  40851  cdleme11  40858  cdleme14  40861  cdleme15a  40862  cdleme15b  40863  cdleme15d  40865  cdleme15  40866  cdleme16b  40867  cdleme16c  40868  cdleme16d  40869  cdleme18d  40883  cdleme19b  40892  cdleme19e  40895  cdleme20d  40900  cdleme20g  40903  cdleme20h  40904  cdleme20i  40905  cdleme20j  40906  cdleme20l2  40909  cdleme20l  40910  cdleme20m  40911  cdleme21c  40915  cdleme21ct  40917  cdleme21d  40918  cdleme21e  40919  cdleme22cN  40930  cdleme22f  40934  cdleme22f2  40935  cdleme23a  40937  cdleme23b  40938  cdleme23c  40939  cdleme25a  40941  cdleme25dN  40944  cdleme26fALTN  40950  cdleme26f  40951  cdleme26f2ALTN  40952  cdleme26f2  40953  cdlemefr29bpre0N  40994  cdlemefr29clN  40995  cdlemefr32fvaN  40997  cdlemefr32fva1  40998  cdleme41sn3a  41021  cdleme32le  41035  cdleme35a  41036  cdleme35fnpq  41037  cdleme35b  41038  cdleme35c  41039  cdleme35d  41040  cdleme35e  41041  cdleme35f  41042  cdleme36a  41048  cdleme37m  41050  cdleme39n  41054  cdleme43bN  41078  cdleme43dN  41080  cdleme17d2  41083  cdlemeg46c  41101  cdlemeg46nlpq  41105  cdlemeg46ngfr  41106  cdlemeg46req  41117  cdlemeg46gfv  41118  cdleme50trn1  41137  cdleme50trn2a  41138  cdlemf1  41149  trlord  41157  cdlemb3  41194  cdlemg7fvbwN  41195  cdlemg7aN  41213  cdlemg10a  41228  cdlemg10  41229  cdlemg12d  41234  cdlemg12e  41235  cdlemg12f  41236  cdlemg12g  41237  cdlemg12  41238  cdlemg13a  41239  cdlemg13  41240  cdlemg17b  41250  cdlemg17f  41254  cdlemg17g  41255  cdlemg17h  41256  cdlemg17pq  41260  cdlemg17  41265  cdlemg19a  41271  cdlemg19  41272  cdlemg21  41274  cdlemg27a  41280  cdlemg27b  41284  cdlemg31c  41287  cdlemg33b0  41289  cdlemg33a  41294  trlcone  41316  cdlemg44  41321  cdlemg48  41325  cdlemk37  41502  cdlemky  41514  cdlemk11ta  41517  cdleml4N  41567  dihord1  41806  dihord2pre2  41814  dihord4  41846  dihord5apre  41850  dihmeetlem1N  41878  dihglblem3N  41883  dihglbcpreN  41888  dihmeetlem3N  41893  dihmeetlem13N  41907  mapdpglem32  42293  baerlem3lem2  42298  baerlem5alem2  42299  baerlem5blem2  42300  mzpcong  43513  iscnrm3rlem8  49532