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

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

Proof of Theorem simp12l
StepHypRef Expression
1 simp2l 1200 . 2 ((𝜒 ∧ (𝜑𝜓) ∧ 𝜃) → 𝜑)
213ad2ant1 1134 1 (((𝜒 ∧ (𝜑𝜓) ∧ 𝜃) ∧ 𝜏𝜂) → 𝜑)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 397  w3a 1088
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 206  df-an 398  df-3an 1090
This theorem is referenced by:  ackbij1lem16  10176  axcontlem4  27958  eqlkr  37607  athgt  37965  llncvrlpln2  38066  4atlem11b  38117  2lnat  38293  cdlemblem  38302  pclfinN  38409  lhp2lt  38510  lhpmcvr5N  38536  lhpmcvr6N  38537  lhp2at0  38541  lhp2atnle  38542  lhp2at0nle  38544  4atexlemex6  38583  cdlemd2  38708  cdlemd7  38713  cdlemd8  38714  cdlemd9  38715  cdleme7aa  38751  cdleme7c  38754  cdleme7d  38755  cdleme7e  38756  cdleme7ga  38757  cdleme7  38758  cdleme11c  38770  cdleme11dN  38771  cdleme11e  38772  cdleme11  38779  cdleme14  38782  cdleme15a  38783  cdleme15b  38784  cdleme15d  38786  cdleme15  38787  cdleme16b  38788  cdleme16c  38789  cdleme16d  38790  cdleme18d  38804  cdleme19b  38813  cdleme19e  38816  cdleme20d  38821  cdleme20g  38824  cdleme20h  38825  cdleme20i  38826  cdleme20j  38827  cdleme20l2  38830  cdleme20l  38831  cdleme20m  38832  cdleme21c  38836  cdleme21ct  38838  cdleme21d  38839  cdleme21e  38840  cdleme22cN  38851  cdleme22f  38855  cdleme22f2  38856  cdleme23a  38858  cdleme23b  38859  cdleme23c  38860  cdleme25a  38862  cdleme25dN  38865  cdleme26fALTN  38871  cdleme26f  38872  cdleme26f2ALTN  38873  cdleme26f2  38874  cdlemefr29bpre0N  38915  cdlemefr29clN  38916  cdlemefr32fvaN  38918  cdlemefr32fva1  38919  cdleme41sn3a  38942  cdleme32le  38956  cdleme35a  38957  cdleme35fnpq  38958  cdleme35b  38959  cdleme35c  38960  cdleme35d  38961  cdleme35e  38962  cdleme35f  38963  cdleme36a  38969  cdleme37m  38971  cdleme39n  38975  cdleme43bN  38999  cdleme43dN  39001  cdleme17d2  39004  cdlemeg46c  39022  cdlemeg46nlpq  39026  cdlemeg46ngfr  39027  cdlemeg46req  39038  cdlemeg46gfv  39039  cdleme50trn1  39058  cdleme50trn2a  39059  cdlemf1  39070  trlord  39078  cdlemb3  39115  cdlemg7fvbwN  39116  cdlemg7aN  39134  cdlemg10a  39149  cdlemg10  39150  cdlemg12d  39155  cdlemg12e  39156  cdlemg12f  39157  cdlemg12g  39158  cdlemg12  39159  cdlemg13a  39160  cdlemg13  39161  cdlemg17b  39171  cdlemg17f  39175  cdlemg17g  39176  cdlemg17h  39177  cdlemg17pq  39181  cdlemg17  39186  cdlemg19a  39192  cdlemg19  39193  cdlemg21  39195  cdlemg27a  39201  cdlemg27b  39205  cdlemg31c  39208  cdlemg33b0  39210  cdlemg33a  39215  trlcone  39237  cdlemg44  39242  cdlemg48  39246  cdlemk37  39423  cdlemky  39435  cdlemk11ta  39438  cdleml4N  39488  dihord1  39727  dihord2pre2  39735  dihord4  39767  dihord5apre  39771  dihmeetlem1N  39799  dihglblem3N  39804  dihglbcpreN  39809  dihmeetlem3N  39814  dihmeetlem13N  39828  mapdpglem32  40214  baerlem3lem2  40219  baerlem5alem2  40220  baerlem5blem2  40221  mzpcong  41339  iscnrm3rlem8  47066
  Copyright terms: Public domain W3C validator