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

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

Proof of Theorem simp12l
StepHypRef Expression
1 simp2l 1242 . 2 ((𝜒 ∧ (𝜑𝜓) ∧ 𝜃) → 𝜑)
213ad2ant1 1128 1 (((𝜒 ∧ (𝜑𝜓) ∧ 𝜃) ∧ 𝜏𝜂) → 𝜑)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 383  w3a 1072
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 385  df-3an 1074
This theorem is referenced by:  ackbij1lem16  9249  axcontlem4  26046  eqlkr  34889  athgt  35245  llncvrlpln2  35346  4atlem11b  35397  2lnat  35573  cdlemblem  35582  pclfinN  35689  lhp2lt  35790  lhpmcvr5N  35816  lhpmcvr6N  35817  lhp2at0  35821  lhp2atnle  35822  lhp2at0nle  35824  4atexlemex6  35863  cdlemd2  35989  cdlemd7  35994  cdlemd8  35995  cdlemd9  35996  cdleme7aa  36032  cdleme7c  36035  cdleme7d  36036  cdleme7e  36037  cdleme7ga  36038  cdleme7  36039  cdleme11c  36051  cdleme11dN  36052  cdleme11e  36053  cdleme11  36060  cdleme14  36063  cdleme15a  36064  cdleme15b  36065  cdleme15d  36067  cdleme15  36068  cdleme16b  36069  cdleme16c  36070  cdleme16d  36071  cdleme18d  36085  cdleme19b  36094  cdleme19e  36097  cdleme20d  36102  cdleme20g  36105  cdleme20h  36106  cdleme20i  36107  cdleme20j  36108  cdleme20l2  36111  cdleme20l  36112  cdleme20m  36113  cdleme21c  36117  cdleme21ct  36119  cdleme21d  36120  cdleme21e  36121  cdleme22cN  36132  cdleme22f  36136  cdleme22f2  36137  cdleme23a  36139  cdleme23b  36140  cdleme23c  36141  cdleme25a  36143  cdleme25dN  36146  cdleme26fALTN  36152  cdleme26f  36153  cdleme26f2ALTN  36154  cdleme26f2  36155  cdlemefr29bpre0N  36196  cdlemefr29clN  36197  cdlemefr32fvaN  36199  cdlemefr32fva1  36200  cdleme41sn3a  36223  cdleme32le  36237  cdleme35a  36238  cdleme35fnpq  36239  cdleme35b  36240  cdleme35c  36241  cdleme35d  36242  cdleme35e  36243  cdleme35f  36244  cdleme36a  36250  cdleme37m  36252  cdleme39n  36256  cdleme43bN  36280  cdleme43dN  36282  cdleme17d2  36285  cdlemeg46c  36303  cdlemeg46nlpq  36307  cdlemeg46ngfr  36308  cdlemeg46req  36319  cdlemeg46gfv  36320  cdleme50trn1  36339  cdleme50trn2a  36340  cdlemf1  36351  trlord  36359  cdlemb3  36396  cdlemg7fvbwN  36397  cdlemg7aN  36415  cdlemg10a  36430  cdlemg10  36431  cdlemg12d  36436  cdlemg12e  36437  cdlemg12f  36438  cdlemg12g  36439  cdlemg12  36440  cdlemg13a  36441  cdlemg13  36442  cdlemg17b  36452  cdlemg17f  36456  cdlemg17g  36457  cdlemg17h  36458  cdlemg17pq  36462  cdlemg17  36467  cdlemg19a  36473  cdlemg19  36474  cdlemg21  36476  cdlemg27a  36482  cdlemg27b  36486  cdlemg31c  36489  cdlemg33b0  36491  cdlemg33a  36496  trlcone  36518  cdlemg44  36523  cdlemg48  36527  cdlemk37  36704  cdlemky  36716  cdlemk11ta  36719  cdleml4N  36769  dihord1  37009  dihord2pre2  37017  dihord4  37049  dihord5apre  37053  dihmeetlem1N  37081  dihglblem3N  37086  dihglbcpreN  37091  dihmeetlem3N  37096  dihmeetlem13N  37110  mapdpglem32  37496  baerlem3lem2  37501  baerlem5alem2  37502  baerlem5blem2  37503  mzpcong  38041
  Copyright terms: Public domain W3C validator