Theorem simp12l 1282

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

Assertion

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

Proof of Theorem simp12l

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

Syntax hints:   → wi 4   ∧ wa 398   ∧ w3a 1083

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 399  df-3an 1085

This theorem is referenced by:  ackbij1lem16  9660  axcontlem4  26756  eqlkr  36239  athgt  36596  llncvrlpln2  36697  4atlem11b  36748  2lnat  36924  cdlemblem  36933  pclfinN  37040  lhp2lt  37141  lhpmcvr5N  37167  lhpmcvr6N  37168  lhp2at0  37172  lhp2atnle  37173  lhp2at0nle  37175  4atexlemex6  37214  cdlemd2  37339  cdlemd7  37344  cdlemd8  37345  cdlemd9  37346  cdleme7aa  37382  cdleme7c  37385  cdleme7d  37386  cdleme7e  37387  cdleme7ga  37388  cdleme7  37389  cdleme11c  37401  cdleme11dN  37402  cdleme11e  37403  cdleme11  37410  cdleme14  37413  cdleme15a  37414  cdleme15b  37415  cdleme15d  37417  cdleme15  37418  cdleme16b  37419  cdleme16c  37420  cdleme16d  37421  cdleme18d  37435  cdleme19b  37444  cdleme19e  37447  cdleme20d  37452  cdleme20g  37455  cdleme20h  37456  cdleme20i  37457  cdleme20j  37458  cdleme20l2  37461  cdleme20l  37462  cdleme20m  37463  cdleme21c  37467  cdleme21ct  37469  cdleme21d  37470  cdleme21e  37471  cdleme22cN  37482  cdleme22f  37486  cdleme22f2  37487  cdleme23a  37489  cdleme23b  37490  cdleme23c  37491  cdleme25a  37493  cdleme25dN  37496  cdleme26fALTN  37502  cdleme26f  37503  cdleme26f2ALTN  37504  cdleme26f2  37505  cdlemefr29bpre0N  37546  cdlemefr29clN  37547  cdlemefr32fvaN  37549  cdlemefr32fva1  37550  cdleme41sn3a  37573  cdleme32le  37587  cdleme35a  37588  cdleme35fnpq  37589  cdleme35b  37590  cdleme35c  37591  cdleme35d  37592  cdleme35e  37593  cdleme35f  37594  cdleme36a  37600  cdleme37m  37602  cdleme39n  37606  cdleme43bN  37630  cdleme43dN  37632  cdleme17d2  37635  cdlemeg46c  37653  cdlemeg46nlpq  37657  cdlemeg46ngfr  37658  cdlemeg46req  37669  cdlemeg46gfv  37670  cdleme50trn1  37689  cdleme50trn2a  37690  cdlemf1  37701  trlord  37709  cdlemb3  37746  cdlemg7fvbwN  37747  cdlemg7aN  37765  cdlemg10a  37780  cdlemg10  37781  cdlemg12d  37786  cdlemg12e  37787  cdlemg12f  37788  cdlemg12g  37789  cdlemg12  37790  cdlemg13a  37791  cdlemg13  37792  cdlemg17b  37802  cdlemg17f  37806  cdlemg17g  37807  cdlemg17h  37808  cdlemg17pq  37812  cdlemg17  37817  cdlemg19a  37823  cdlemg19  37824  cdlemg21  37826  cdlemg27a  37832  cdlemg27b  37836  cdlemg31c  37839  cdlemg33b0  37841  cdlemg33a  37846  trlcone  37868  cdlemg44  37873  cdlemg48  37877  cdlemk37  38054  cdlemky  38066  cdlemk11ta  38069  cdleml4N  38119  dihord1  38358  dihord2pre2  38366  dihord4  38398  dihord5apre  38402  dihmeetlem1N  38430  dihglblem3N  38435  dihglbcpreN  38440  dihmeetlem3N  38445  dihmeetlem13N  38459  mapdpglem32  38845  baerlem3lem2  38850  baerlem5alem2  38851  baerlem5blem2  38852  mzpcong  39575