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

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

Proof of Theorem simp12l
StepHypRef Expression
1 simp2l 1085 . 2 ((𝜒 ∧ (𝜑𝜓) ∧ 𝜃) → 𝜑)
213ad2ant1 1080 1 (((𝜒 ∧ (𝜑𝜓) ∧ 𝜃) ∧ 𝜏𝜂) → 𝜑)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 384  w3a 1036
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 197  df-an 386  df-3an 1038
This theorem is referenced by:  ackbij1lem16  9001  axcontlem4  25747  eqlkr  33866  athgt  34222  llncvrlpln2  34323  4atlem11b  34374  2lnat  34550  cdlemblem  34559  pclfinN  34666  lhp2lt  34767  lhpmcvr5N  34793  lhpmcvr6N  34794  lhp2at0  34798  lhp2atnle  34799  lhp2at0nle  34801  4atexlemex6  34840  cdlemd2  34966  cdlemd7  34971  cdlemd8  34972  cdlemd9  34973  cdleme7aa  35009  cdleme7c  35012  cdleme7d  35013  cdleme7e  35014  cdleme7ga  35015  cdleme7  35016  cdleme11c  35028  cdleme11dN  35029  cdleme11e  35030  cdleme11  35037  cdleme14  35040  cdleme15a  35041  cdleme15b  35042  cdleme15d  35044  cdleme15  35045  cdleme16b  35046  cdleme16c  35047  cdleme16d  35048  cdleme18d  35062  cdleme19b  35072  cdleme19e  35075  cdleme20d  35080  cdleme20g  35083  cdleme20h  35084  cdleme20i  35085  cdleme20j  35086  cdleme20l2  35089  cdleme20l  35090  cdleme20m  35091  cdleme21c  35095  cdleme21ct  35097  cdleme21d  35098  cdleme21e  35099  cdleme22cN  35110  cdleme22f  35114  cdleme22f2  35115  cdleme23a  35117  cdleme23b  35118  cdleme23c  35119  cdleme25a  35121  cdleme25dN  35124  cdleme26fALTN  35130  cdleme26f  35131  cdleme26f2ALTN  35132  cdleme26f2  35133  cdlemefr29bpre0N  35174  cdlemefr29clN  35175  cdlemefr32fvaN  35177  cdlemefr32fva1  35178  cdleme41sn3a  35201  cdleme32le  35215  cdleme35a  35216  cdleme35fnpq  35217  cdleme35b  35218  cdleme35c  35219  cdleme35d  35220  cdleme35e  35221  cdleme35f  35222  cdleme36a  35228  cdleme37m  35230  cdleme39n  35234  cdleme43bN  35258  cdleme43dN  35260  cdleme17d2  35263  cdlemeg46c  35281  cdlemeg46nlpq  35285  cdlemeg46ngfr  35286  cdlemeg46req  35297  cdlemeg46gfv  35298  cdleme50trn1  35317  cdleme50trn2a  35318  cdlemf1  35329  trlord  35337  cdlemb3  35374  cdlemg7fvbwN  35375  cdlemg7aN  35393  cdlemg10a  35408  cdlemg10  35409  cdlemg12d  35414  cdlemg12e  35415  cdlemg12f  35416  cdlemg12g  35417  cdlemg12  35418  cdlemg13a  35419  cdlemg13  35420  cdlemg17b  35430  cdlemg17f  35434  cdlemg17g  35435  cdlemg17h  35436  cdlemg17pq  35440  cdlemg17  35445  cdlemg19a  35451  cdlemg19  35452  cdlemg21  35454  cdlemg27a  35460  cdlemg27b  35464  cdlemg31c  35467  cdlemg33b0  35469  cdlemg33a  35474  trlcone  35496  cdlemg44  35501  cdlemg48  35505  cdlemk37  35682  cdlemky  35694  cdlemk11ta  35697  cdleml4N  35747  dihord1  35987  dihord2pre2  35995  dihord4  36027  dihord5apre  36031  dihmeetlem1N  36059  dihglblem3N  36064  dihglbcpreN  36069  dihmeetlem3N  36074  dihmeetlem13N  36088  mapdpglem32  36474  baerlem3lem2  36479  baerlem5alem2  36480  baerlem5blem2  36481  mzpcong  37019
  Copyright terms: Public domain W3C validator