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

Theorem simp13l 1103
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 1016 . 2  |-  ( ( ch  /\  th  /\  ( ph  /\  ps )
)  ->  ph )
213ad2ant1 1009 1  |-  ( ( ( ch  /\  th  /\  ( ph  /\  ps ) )  /\  ta  /\  et )  ->  ph )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369    /\ w3a 965
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 967
This theorem is referenced by:  pceu  13905  axpasch  23155  mzpcong  29286  3atlem4  33023  llncvrlpln2  33094  2lplnja  33156  2lnat  33321  llnexchb2  33406  lhp2lt  33538  lhpmcvr5N  33564  4atexlemq  33588  4atexlemex6  33611  trlval2  33700  cdleme7d  33783  cdleme7e  33784  cdleme7ga  33785  cdleme7  33786  cdleme11l  33806  cdleme11  33807  cdleme14  33810  cdleme15a  33811  cdleme15b  33812  cdleme15  33815  cdleme16b  33816  cdleme16c  33817  cdleme16d  33818  cdleme18d  33832  cdleme19b  33841  cdleme19e  33844  cdleme20d  33849  cdleme20g  33852  cdleme20h  33853  cdleme20i  33854  cdleme20j  33855  cdleme20l2  33858  cdleme20l  33859  cdleme20m  33860  cdleme21d  33867  cdleme21e  33868  cdleme21h  33871  cdleme22f  33883  cdleme23a  33886  cdleme23b  33887  cdleme23c  33888  cdleme24  33889  cdleme25a  33890  cdleme25dN  33893  cdleme26ee  33897  cdleme26fALTN  33899  cdleme26f  33900  cdleme26f2ALTN  33901  cdleme26f2  33902  cdleme27a  33904  cdlemefr29bpre0N  33943  cdlemefr29clN  33944  cdlemefr32fvaN  33946  cdlemefr32fva1  33947  cdleme41sn3a  33970  cdleme35a  33985  cdleme35fnpq  33986  cdleme35b  33987  cdleme35c  33988  cdleme35d  33989  cdleme35f  33991  cdleme36m  33998  cdleme37m  33999  cdleme39n  34003  cdleme43bN  34027  cdleme43dN  34029  cdleme17d2  34032  cdlemeg46c  34050  cdlemeg46nlpq  34054  cdlemeg46ngfr  34055  cdlemeg46req  34066  cdlemeg46gfv  34067  cdleme50trn1  34086  cdleme50trn2a  34087  cdlemf1  34098  cdlemf  34100  cdlemg10a  34177  cdlemg10  34178  cdlemg12d  34183  cdlemg12e  34184  cdlemg12f  34185  cdlemg12g  34186  cdlemg12  34187  cdlemg13  34189  cdlemg16ALTN  34195  cdlemg17b  34199  cdlemg17h  34205  cdlemg17pq  34209  cdlemg17iqN  34211  cdlemg17  34214  cdlemg19a  34220  cdlemg19  34221  cdlemg21  34223  cdlemg27a  34229  cdlemg27b  34233  cdlemg31c  34236  cdlemg33b0  34238  cdlemg33a  34243  cdlemg48  34274  tendocan  34361  cdlemk26-3  34443  cdlemk27-3  34444  cdlemk28-3  34445  cdlemk37  34451  cdlemky  34463  cdlemkyu  34464  cdlemk11ta  34466  cdlemkid3N  34470  cdlemk42  34478  cdlemk42yN  34481  cdlemk11t  34483  cdlemk45  34484  cdlemk46  34485  cdlemk47  34486  cdlemk51  34490  cdlemk52  34491  cdlemk53a  34492  cdleml4N  34516  dihord2pre2  34764  dihord4  34796  dihord5apre  34800  dihmeetlem1N  34828  dihmeetlem15N  34859  mapdpglem32  35243
  Copyright terms: Public domain W3C validator