MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  simp12l Structured version   Visualization version   GIF version

Theorem simp12l 1167
Description: Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
Assertion
Ref Expression
simp12l (((𝜒 ∧ (𝜑𝜓) ∧ 𝜃) ∧ 𝜏𝜂) → 𝜑)

Proof of Theorem simp12l
StepHypRef Expression
1 simp2l 1080 . 2 ((𝜒 ∧ (𝜑𝜓) ∧ 𝜃) → 𝜑)
213ad2ant1 1075 1 (((𝜒 ∧ (𝜑𝜓) ∧ 𝜃) ∧ 𝜏𝜂) → 𝜑)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 383  w3a 1031
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 196  df-an 385  df-3an 1033
This theorem is referenced by:  ackbij1lem16  8940  axcontlem4  25647  eqlkr  33404  athgt  33760  llncvrlpln2  33861  4atlem11b  33912  2lnat  34088  cdlemblem  34097  pclfinN  34204  lhp2lt  34305  lhpmcvr5N  34331  lhpmcvr6N  34332  lhp2at0  34336  lhp2atnle  34337  lhp2at0nle  34339  4atexlemex6  34378  cdlemd2  34504  cdlemd7  34509  cdlemd8  34510  cdlemd9  34511  cdleme7aa  34547  cdleme7c  34550  cdleme7d  34551  cdleme7e  34552  cdleme7ga  34553  cdleme7  34554  cdleme11c  34566  cdleme11dN  34567  cdleme11e  34568  cdleme11  34575  cdleme14  34578  cdleme15a  34579  cdleme15b  34580  cdleme15d  34582  cdleme15  34583  cdleme16b  34584  cdleme16c  34585  cdleme16d  34586  cdleme18d  34600  cdleme19b  34610  cdleme19e  34613  cdleme20d  34618  cdleme20g  34621  cdleme20h  34622  cdleme20i  34623  cdleme20j  34624  cdleme20l2  34627  cdleme20l  34628  cdleme20m  34629  cdleme21c  34633  cdleme21ct  34635  cdleme21d  34636  cdleme21e  34637  cdleme22cN  34648  cdleme22f  34652  cdleme22f2  34653  cdleme23a  34655  cdleme23b  34656  cdleme23c  34657  cdleme25a  34659  cdleme25dN  34662  cdleme26fALTN  34668  cdleme26f  34669  cdleme26f2ALTN  34670  cdleme26f2  34671  cdlemefr29bpre0N  34712  cdlemefr29clN  34713  cdlemefr32fvaN  34715  cdlemefr32fva1  34716  cdleme41sn3a  34739  cdleme32le  34753  cdleme35a  34754  cdleme35fnpq  34755  cdleme35b  34756  cdleme35c  34757  cdleme35d  34758  cdleme35e  34759  cdleme35f  34760  cdleme36a  34766  cdleme37m  34768  cdleme39n  34772  cdleme43bN  34796  cdleme43dN  34798  cdleme17d2  34801  cdlemeg46c  34819  cdlemeg46nlpq  34823  cdlemeg46ngfr  34824  cdlemeg46req  34835  cdlemeg46gfv  34836  cdleme50trn1  34855  cdleme50trn2a  34856  cdlemf1  34867  trlord  34875  cdlemb3  34912  cdlemg7fvbwN  34913  cdlemg7aN  34931  cdlemg10a  34946  cdlemg10  34947  cdlemg12d  34952  cdlemg12e  34953  cdlemg12f  34954  cdlemg12g  34955  cdlemg12  34956  cdlemg13a  34957  cdlemg13  34958  cdlemg17b  34968  cdlemg17f  34972  cdlemg17g  34973  cdlemg17h  34974  cdlemg17pq  34978  cdlemg17  34983  cdlemg19a  34989  cdlemg19  34990  cdlemg21  34992  cdlemg27a  34998  cdlemg27b  35002  cdlemg31c  35005  cdlemg33b0  35007  cdlemg33a  35012  trlcone  35034  cdlemg44  35039  cdlemg48  35043  cdlemk37  35220  cdlemky  35232  cdlemk11ta  35235  cdleml4N  35285  dihord1  35525  dihord2pre2  35533  dihord4  35565  dihord5apre  35569  dihmeetlem1N  35597  dihglblem3N  35602  dihglbcpreN  35607  dihmeetlem3N  35612  dihmeetlem13N  35626  mapdpglem32  36012  baerlem3lem2  36017  baerlem5alem2  36018  baerlem5blem2  36019  mzpcong  36557
  Copyright terms: Public domain W3C validator