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

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

Proof of Theorem simp13l
StepHypRef Expression
1 simp3l 1023 . 2  |-  ( ( ch  /\  th  /\  ( ph  /\  ps )
)  ->  ph )
213ad2ant1 1016 1  |-  ( ( ( ch  /\  th  /\  ( ph  /\  ps ) )  /\  ta  /\  et )  ->  ph )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369    /\ w3a 972
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 185  df-an 371  df-3an 974
This theorem is referenced by:  pceu  14244  axpasch  24113  mzpcong  30882  mullimc  31530  mullimcf  31537  addlimc  31562  3atlem4  34933  llncvrlpln2  35004  2lplnja  35066  2lnat  35231  llnexchb2  35316  lhp2lt  35448  lhpmcvr5N  35474  4atexlemq  35498  4atexlemex6  35521  trlval2  35611  cdleme7d  35694  cdleme7e  35695  cdleme7ga  35696  cdleme7  35697  cdleme11l  35717  cdleme11  35718  cdleme14  35721  cdleme15a  35722  cdleme15b  35723  cdleme15  35726  cdleme16b  35727  cdleme16c  35728  cdleme16d  35729  cdleme18d  35743  cdleme19b  35753  cdleme19e  35756  cdleme20d  35761  cdleme20g  35764  cdleme20h  35765  cdleme20i  35766  cdleme20j  35767  cdleme20l2  35770  cdleme20l  35771  cdleme20m  35772  cdleme21d  35779  cdleme21e  35780  cdleme21h  35783  cdleme22f  35795  cdleme23a  35798  cdleme23b  35799  cdleme23c  35800  cdleme24  35801  cdleme25a  35802  cdleme25dN  35805  cdleme26ee  35809  cdleme26fALTN  35811  cdleme26f  35812  cdleme26f2ALTN  35813  cdleme26f2  35814  cdleme27a  35816  cdlemefr29bpre0N  35855  cdlemefr29clN  35856  cdlemefr32fvaN  35858  cdlemefr32fva1  35859  cdleme41sn3a  35882  cdleme35a  35897  cdleme35fnpq  35898  cdleme35b  35899  cdleme35c  35900  cdleme35d  35901  cdleme35f  35903  cdleme36m  35910  cdleme37m  35911  cdleme39n  35915  cdleme43bN  35939  cdleme43dN  35941  cdleme17d2  35944  cdlemeg46c  35962  cdlemeg46nlpq  35966  cdlemeg46ngfr  35967  cdlemeg46req  35978  cdlemeg46gfv  35979  cdleme50trn1  35998  cdleme50trn2a  35999  cdlemf1  36010  cdlemf  36012  cdlemg10a  36089  cdlemg10  36090  cdlemg12d  36095  cdlemg12e  36096  cdlemg12f  36097  cdlemg12g  36098  cdlemg12  36099  cdlemg13  36101  cdlemg16ALTN  36107  cdlemg17b  36111  cdlemg17h  36117  cdlemg17pq  36121  cdlemg17iqN  36123  cdlemg17  36126  cdlemg19a  36132  cdlemg19  36133  cdlemg21  36135  cdlemg27a  36141  cdlemg27b  36145  cdlemg31c  36148  cdlemg33b0  36150  cdlemg33a  36155  cdlemg48  36186  tendocan  36273  cdlemk26-3  36355  cdlemk27-3  36356  cdlemk28-3  36357  cdlemk37  36363  cdlemky  36375  cdlemkyu  36376  cdlemk11ta  36378  cdlemkid3N  36382  cdlemk42  36390  cdlemk42yN  36393  cdlemk11t  36395  cdlemk45  36396  cdlemk46  36397  cdlemk47  36398  cdlemk51  36402  cdlemk52  36403  cdlemk53a  36404  cdleml4N  36428  dihord2pre2  36676  dihord4  36708  dihord5apre  36712  dihmeetlem1N  36740  dihmeetlem15N  36771  mapdpglem32  37155
  Copyright terms: Public domain W3C validator