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

Theorem simp12l 1071
Description: Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
Assertion
Ref Expression
simp12l  |-  ( ( ( ch  /\  ( ph  /\  ps )  /\  th )  /\  ta  /\  et )  ->  ph )

Proof of Theorem simp12l
StepHypRef Expression
1 simp2l 984 . 2  |-  ( ( ch  /\  ( ph  /\ 
ps )  /\  th )  ->  ph )
213ad2ant1 979 1  |-  ( ( ( ch  /\  ( ph  /\  ps )  /\  th )  /\  ta  /\  et )  ->  ph )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 360    /\ w3a 937
This theorem is referenced by:  ackbij1lem16  8117  axcontlem4  25908  mzpcong  27039  eqlkr  29899  athgt  30255  llncvrlpln2  30356  4atlem11b  30407  2lnat  30583  cdlemblem  30592  pclfinN  30699  lhp2lt  30800  lhpmcvr5N  30826  lhpmcvr6N  30827  lhp2at0  30831  lhp2atnle  30832  lhp2at0nle  30834  4atexlemex6  30873  cdlemd2  30998  cdlemd7  31003  cdlemd8  31004  cdlemd9  31005  cdleme7aa  31041  cdleme7c  31044  cdleme7d  31045  cdleme7e  31046  cdleme7ga  31047  cdleme7  31048  cdleme11c  31060  cdleme11dN  31061  cdleme11e  31062  cdleme11  31069  cdleme14  31072  cdleme15a  31073  cdleme15b  31074  cdleme15d  31076  cdleme15  31077  cdleme16b  31078  cdleme16c  31079  cdleme16d  31080  cdleme18d  31094  cdleme19b  31103  cdleme19e  31106  cdleme20d  31111  cdleme20g  31114  cdleme20h  31115  cdleme20i  31116  cdleme20j  31117  cdleme20l2  31120  cdleme20l  31121  cdleme20m  31122  cdleme21c  31126  cdleme21ct  31128  cdleme21d  31129  cdleme21e  31130  cdleme22cN  31141  cdleme22f  31145  cdleme22f2  31146  cdleme23a  31148  cdleme23b  31149  cdleme23c  31150  cdleme25a  31152  cdleme25dN  31155  cdleme26fALTN  31161  cdleme26f  31162  cdleme26f2ALTN  31163  cdleme26f2  31164  cdlemefr29bpre0N  31205  cdlemefr29clN  31206  cdlemefr32fvaN  31208  cdlemefr32fva1  31209  cdleme41sn3a  31232  cdleme32le  31246  cdleme35a  31247  cdleme35fnpq  31248  cdleme35b  31249  cdleme35c  31250  cdleme35d  31251  cdleme35e  31252  cdleme35f  31253  cdleme36a  31259  cdleme37m  31261  cdleme39n  31265  cdleme43bN  31289  cdleme43dN  31291  cdleme17d2  31294  cdlemeg46c  31312  cdlemeg46nlpq  31316  cdlemeg46ngfr  31317  cdlemeg46req  31328  cdlemeg46gfv  31329  cdleme50trn1  31348  cdleme50trn2a  31349  cdlemf1  31360  trlord  31368  cdlemb3  31405  cdlemg7fvbwN  31406  cdlemg7aN  31424  cdlemg10a  31439  cdlemg10  31440  cdlemg12d  31445  cdlemg12e  31446  cdlemg12f  31447  cdlemg12g  31448  cdlemg12  31449  cdlemg13a  31450  cdlemg13  31451  cdlemg17b  31461  cdlemg17f  31465  cdlemg17g  31466  cdlemg17h  31467  cdlemg17pq  31471  cdlemg17  31476  cdlemg19a  31482  cdlemg19  31483  cdlemg21  31485  cdlemg27a  31491  cdlemg27b  31495  cdlemg31c  31498  cdlemg33b0  31500  cdlemg33a  31505  trlcone  31527  cdlemg44  31532  cdlemg48  31536  cdlemk37  31713  cdlemky  31725  cdlemk11ta  31728  cdleml4N  31778  dihord1  32018  dihord2pre2  32026  dihord4  32058  dihord5apre  32062  dihmeetlem1N  32090  dihglblem3N  32095  dihglbcpreN  32100  dihmeetlem3N  32105  dihmeetlem13N  32119  mapdpglem32  32505  baerlem3lem2  32510  baerlem5alem2  32511  baerlem5blem2  32512
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 179  df-an 362  df-3an 939
  Copyright terms: Public domain W3C validator