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

Theorem simp13l 1111
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 1024 . 2  |-  ( ( ch  /\  th  /\  ( ph  /\  ps )
)  ->  ph )
213ad2ant1 1017 1  |-  ( ( ( ch  /\  th  /\  ( ph  /\  ps ) )  /\  ta  /\  et )  ->  ph )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369    /\ w3a 973
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 975
This theorem is referenced by:  pceu  14225  axpasch  23920  mzpcong  30514  mullimc  31158  mullimcf  31165  addlimc  31190  3atlem4  34282  llncvrlpln2  34353  2lplnja  34415  2lnat  34580  llnexchb2  34665  lhp2lt  34797  lhpmcvr5N  34823  4atexlemq  34847  4atexlemex6  34870  trlval2  34959  cdleme7d  35042  cdleme7e  35043  cdleme7ga  35044  cdleme7  35045  cdleme11l  35065  cdleme11  35066  cdleme14  35069  cdleme15a  35070  cdleme15b  35071  cdleme15  35074  cdleme16b  35075  cdleme16c  35076  cdleme16d  35077  cdleme18d  35091  cdleme19b  35100  cdleme19e  35103  cdleme20d  35108  cdleme20g  35111  cdleme20h  35112  cdleme20i  35113  cdleme20j  35114  cdleme20l2  35117  cdleme20l  35118  cdleme20m  35119  cdleme21d  35126  cdleme21e  35127  cdleme21h  35130  cdleme22f  35142  cdleme23a  35145  cdleme23b  35146  cdleme23c  35147  cdleme24  35148  cdleme25a  35149  cdleme25dN  35152  cdleme26ee  35156  cdleme26fALTN  35158  cdleme26f  35159  cdleme26f2ALTN  35160  cdleme26f2  35161  cdleme27a  35163  cdlemefr29bpre0N  35202  cdlemefr29clN  35203  cdlemefr32fvaN  35205  cdlemefr32fva1  35206  cdleme41sn3a  35229  cdleme35a  35244  cdleme35fnpq  35245  cdleme35b  35246  cdleme35c  35247  cdleme35d  35248  cdleme35f  35250  cdleme36m  35257  cdleme37m  35258  cdleme39n  35262  cdleme43bN  35286  cdleme43dN  35288  cdleme17d2  35291  cdlemeg46c  35309  cdlemeg46nlpq  35313  cdlemeg46ngfr  35314  cdlemeg46req  35325  cdlemeg46gfv  35326  cdleme50trn1  35345  cdleme50trn2a  35346  cdlemf1  35357  cdlemf  35359  cdlemg10a  35436  cdlemg10  35437  cdlemg12d  35442  cdlemg12e  35443  cdlemg12f  35444  cdlemg12g  35445  cdlemg12  35446  cdlemg13  35448  cdlemg16ALTN  35454  cdlemg17b  35458  cdlemg17h  35464  cdlemg17pq  35468  cdlemg17iqN  35470  cdlemg17  35473  cdlemg19a  35479  cdlemg19  35480  cdlemg21  35482  cdlemg27a  35488  cdlemg27b  35492  cdlemg31c  35495  cdlemg33b0  35497  cdlemg33a  35502  cdlemg48  35533  tendocan  35620  cdlemk26-3  35702  cdlemk27-3  35703  cdlemk28-3  35704  cdlemk37  35710  cdlemky  35722  cdlemkyu  35723  cdlemk11ta  35725  cdlemkid3N  35729  cdlemk42  35737  cdlemk42yN  35740  cdlemk11t  35742  cdlemk45  35743  cdlemk46  35744  cdlemk47  35745  cdlemk51  35749  cdlemk52  35750  cdlemk53a  35751  cdleml4N  35775  dihord2pre2  36023  dihord4  36055  dihord5apre  36059  dihmeetlem1N  36087  dihmeetlem15N  36118  mapdpglem32  36502
  Copyright terms: Public domain W3C validator