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

Theorem simp13l 1072
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 985 . 2  |-  ( ( ch  /\  th  /\  ( ph  /\  ps )
)  ->  ph )
213ad2ant1 978 1  |-  ( ( ( ch  /\  th  /\  ( ph  /\  ps ) )  /\  ta  /\  et )  ->  ph )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 359    /\ w3a 936
This theorem is referenced by:  pceu  13175  axpasch  25784  mzpcong  26927  3atlem4  29968  llncvrlpln2  30039  2lplnja  30101  2lnat  30266  llnexchb2  30351  lhp2lt  30483  lhpmcvr5N  30509  4atexlemq  30533  4atexlemex6  30556  trlval2  30645  cdleme7d  30728  cdleme7e  30729  cdleme7ga  30730  cdleme7  30731  cdleme11l  30751  cdleme11  30752  cdleme14  30755  cdleme15a  30756  cdleme15b  30757  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  cdleme21d  30812  cdleme21e  30813  cdleme21h  30816  cdleme22f  30828  cdleme23a  30831  cdleme23b  30832  cdleme23c  30833  cdleme24  30834  cdleme25a  30835  cdleme25dN  30838  cdleme26ee  30842  cdleme26fALTN  30844  cdleme26f  30845  cdleme26f2ALTN  30846  cdleme26f2  30847  cdleme27a  30849  cdlemefr29bpre0N  30888  cdlemefr29clN  30889  cdlemefr32fvaN  30891  cdlemefr32fva1  30892  cdleme41sn3a  30915  cdleme35a  30930  cdleme35fnpq  30931  cdleme35b  30932  cdleme35c  30933  cdleme35d  30934  cdleme35f  30936  cdleme36m  30943  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  cdlemf  31045  cdlemg10a  31122  cdlemg10  31123  cdlemg12d  31128  cdlemg12e  31129  cdlemg12f  31130  cdlemg12g  31131  cdlemg12  31132  cdlemg13  31134  cdlemg16ALTN  31140  cdlemg17b  31144  cdlemg17h  31150  cdlemg17pq  31154  cdlemg17iqN  31156  cdlemg17  31159  cdlemg19a  31165  cdlemg19  31166  cdlemg21  31168  cdlemg27a  31174  cdlemg27b  31178  cdlemg31c  31181  cdlemg33b0  31183  cdlemg33a  31188  cdlemg48  31219  tendocan  31306  cdlemk26-3  31388  cdlemk27-3  31389  cdlemk28-3  31390  cdlemk37  31396  cdlemky  31408  cdlemkyu  31409  cdlemk11ta  31411  cdlemkid3N  31415  cdlemk42  31423  cdlemk42yN  31426  cdlemk11t  31428  cdlemk45  31429  cdlemk46  31430  cdlemk47  31431  cdlemk51  31435  cdlemk52  31436  cdlemk53a  31437  cdleml4N  31461  dihord2pre2  31709  dihord4  31741  dihord5apre  31745  dihmeetlem1N  31773  dihmeetlem15N  31804  mapdpglem32  32188
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