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

Theorem simp12l 1070
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 983 . 2  |-  ( ( ch  /\  ( ph  /\ 
ps )  /\  th )  ->  ph )
213ad2ant1 978 1  |-  ( ( ( ch  /\  ( ph  /\  ps )  /\  th )  /\  ta  /\  et )  ->  ph )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 359    /\ w3a 936
This theorem is referenced by:  ackbij1lem16  8071  axcontlem4  25810  mzpcong  26927  eqlkr  29582  athgt  29938  llncvrlpln2  30039  4atlem11b  30090  2lnat  30266  cdlemblem  30275  pclfinN  30382  lhp2lt  30483  lhpmcvr5N  30509  lhpmcvr6N  30510  lhp2at0  30514  lhp2atnle  30515  lhp2at0nle  30517  4atexlemex6  30556  cdlemd2  30681  cdlemd7  30686  cdlemd8  30687  cdlemd9  30688  cdleme7aa  30724  cdleme7c  30727  cdleme7d  30728  cdleme7e  30729  cdleme7ga  30730  cdleme7  30731  cdleme11c  30743  cdleme11dN  30744  cdleme11e  30745  cdleme11  30752  cdleme14  30755  cdleme15a  30756  cdleme15b  30757  cdleme15d  30759  cdleme15  30760  cdleme16b  30761  cdleme16c  30762  cdleme16d  30763  cdleme18d  30777  cdleme19b  30786  cdleme19e  30789  cdleme20d  30794  cdleme20g  30797  cdleme20h  30798  cdleme20i  30799  cdleme20j  30800  cdleme20l2  30803  cdleme20l  30804  cdleme20m  30805  cdleme21c  30809  cdleme21ct  30811  cdleme21d  30812  cdleme21e  30813  cdleme22cN  30824  cdleme22f  30828  cdleme22f2  30829  cdleme23a  30831  cdleme23b  30832  cdleme23c  30833  cdleme25a  30835  cdleme25dN  30838  cdleme26fALTN  30844  cdleme26f  30845  cdleme26f2ALTN  30846  cdleme26f2  30847  cdlemefr29bpre0N  30888  cdlemefr29clN  30889  cdlemefr32fvaN  30891  cdlemefr32fva1  30892  cdleme41sn3a  30915  cdleme32le  30929  cdleme35a  30930  cdleme35fnpq  30931  cdleme35b  30932  cdleme35c  30933  cdleme35d  30934  cdleme35e  30935  cdleme35f  30936  cdleme36a  30942  cdleme37m  30944  cdleme39n  30948  cdleme43bN  30972  cdleme43dN  30974  cdleme17d2  30977  cdlemeg46c  30995  cdlemeg46nlpq  30999  cdlemeg46ngfr  31000  cdlemeg46req  31011  cdlemeg46gfv  31012  cdleme50trn1  31031  cdleme50trn2a  31032  cdlemf1  31043  trlord  31051  cdlemb3  31088  cdlemg7fvbwN  31089  cdlemg7aN  31107  cdlemg10a  31122  cdlemg10  31123  cdlemg12d  31128  cdlemg12e  31129  cdlemg12f  31130  cdlemg12g  31131  cdlemg12  31132  cdlemg13a  31133  cdlemg13  31134  cdlemg17b  31144  cdlemg17f  31148  cdlemg17g  31149  cdlemg17h  31150  cdlemg17pq  31154  cdlemg17  31159  cdlemg19a  31165  cdlemg19  31166  cdlemg21  31168  cdlemg27a  31174  cdlemg27b  31178  cdlemg31c  31181  cdlemg33b0  31183  cdlemg33a  31188  trlcone  31210  cdlemg44  31215  cdlemg48  31219  cdlemk37  31396  cdlemky  31408  cdlemk11ta  31411  cdleml4N  31461  dihord1  31701  dihord2pre2  31709  dihord4  31741  dihord5apre  31745  dihmeetlem1N  31773  dihglblem3N  31778  dihglbcpreN  31783  dihmeetlem3N  31788  dihmeetlem13N  31802  mapdpglem32  32188  baerlem3lem2  32193  baerlem5alem2  32194  baerlem5blem2  32195
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 178  df-an 361  df-3an 938
  Copyright terms: Public domain W3C validator