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

Theorem simp13l 1120
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 1033 . 2  |-  ( ( ch  /\  th  /\  ( ph  /\  ps )
)  ->  ph )
213ad2ant1 1026 1  |-  ( ( ( ch  /\  th  /\  ( ph  /\  ps ) )  /\  ta  /\  et )  ->  ph )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 370    /\ w3a 982
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 188  df-an 372  df-3an 984
This theorem is referenced by:  pceu  14756  axpasch  24858  3atlem4  32804  llncvrlpln2  32875  2lplnja  32937  2lnat  33102  llnexchb2  33187  lhp2lt  33319  lhpmcvr5N  33345  4atexlemq  33369  4atexlemex6  33392  trlval2  33482  cdleme7d  33565  cdleme7e  33566  cdleme7ga  33567  cdleme7  33568  cdleme11l  33588  cdleme11  33589  cdleme14  33592  cdleme15a  33593  cdleme15b  33594  cdleme15  33597  cdleme16b  33598  cdleme16c  33599  cdleme16d  33600  cdleme18d  33614  cdleme19b  33624  cdleme19e  33627  cdleme20d  33632  cdleme20g  33635  cdleme20h  33636  cdleme20i  33637  cdleme20j  33638  cdleme20l2  33641  cdleme20l  33642  cdleme20m  33643  cdleme21d  33650  cdleme21e  33651  cdleme21h  33654  cdleme22f  33666  cdleme23a  33669  cdleme23b  33670  cdleme23c  33671  cdleme24  33672  cdleme25a  33673  cdleme25dN  33676  cdleme26ee  33680  cdleme26fALTN  33682  cdleme26f  33683  cdleme26f2ALTN  33684  cdleme26f2  33685  cdleme27a  33687  cdlemefr29bpre0N  33726  cdlemefr29clN  33727  cdlemefr32fvaN  33729  cdlemefr32fva1  33730  cdleme41sn3a  33753  cdleme35a  33768  cdleme35fnpq  33769  cdleme35b  33770  cdleme35c  33771  cdleme35d  33772  cdleme35f  33774  cdleme36m  33781  cdleme37m  33782  cdleme39n  33786  cdleme43bN  33810  cdleme43dN  33812  cdleme17d2  33815  cdlemeg46c  33833  cdlemeg46nlpq  33837  cdlemeg46ngfr  33838  cdlemeg46req  33849  cdlemeg46gfv  33850  cdleme50trn1  33869  cdleme50trn2a  33870  cdlemf1  33881  cdlemf  33883  cdlemg10a  33960  cdlemg10  33961  cdlemg12d  33966  cdlemg12e  33967  cdlemg12f  33968  cdlemg12g  33969  cdlemg12  33970  cdlemg13  33972  cdlemg16ALTN  33978  cdlemg17b  33982  cdlemg17h  33988  cdlemg17pq  33992  cdlemg17iqN  33994  cdlemg17  33997  cdlemg19a  34003  cdlemg19  34004  cdlemg21  34006  cdlemg27a  34012  cdlemg27b  34016  cdlemg31c  34019  cdlemg33b0  34021  cdlemg33a  34026  cdlemg48  34057  tendocan  34144  cdlemk26-3  34226  cdlemk27-3  34227  cdlemk28-3  34228  cdlemk37  34234  cdlemky  34246  cdlemkyu  34247  cdlemk11ta  34249  cdlemkid3N  34253  cdlemk42  34261  cdlemk42yN  34264  cdlemk11t  34266  cdlemk45  34267  cdlemk46  34268  cdlemk47  34269  cdlemk51  34273  cdlemk52  34274  cdlemk53a  34275  cdleml4N  34299  dihord2pre2  34547  dihord4  34579  dihord5apre  34583  dihmeetlem1N  34611  dihmeetlem15N  34642  mapdpglem32  35026  mzpcong  35576  mullimc  37316  mullimcf  37323  addlimc  37349
  Copyright terms: Public domain W3C validator