ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  syl5 Unicode version

Theorem syl5 32
Description: A syllogism rule of inference. The second premise is used to replace the second antecedent of the first premise. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 25-May-2013.)
Hypotheses
Ref Expression
syl5.1  |-  ( ph  ->  ps )
syl5.2  |-  ( ch 
->  ( ps  ->  th )
)
Assertion
Ref Expression
syl5  |-  ( ch 
->  ( ph  ->  th )
)

Proof of Theorem syl5
StepHypRef Expression
1 syl5.1 . . 3  |-  ( ph  ->  ps )
2 syl5.2 . . 3  |-  ( ch 
->  ( ps  ->  th )
)
31, 2syl5com 29 . 2  |-  ( ph  ->  ( ch  ->  th )
)
43com12 30 1  |-  ( ch 
->  ( ph  ->  th )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7
This theorem is referenced by:  syl56  34  syl2im  38  imim12i  59  pm2.86d  99  syl5bi  151  syl5bir  152  syl5ib  153  adantld  274  adantrd  275  impel  276  mpan9  277  nsyli  621  pm2.36  776  pm4.72  795  const  820  pm2.18dc  823  con1dc  824  jadc  831  pm2.521dcALT  838  con1biimdc  841  condandc  849  pm5.18dc  851  pm2.68dc  862  annimdc  904  syl3an2  1233  syl2an23an  1260  xor3dc  1348  alrimdh  1438  spsd  1501  a5i  1505  19.21h  1519  hbnt  1614  hbae  1679  sbiedh  1743  exdistrfor  1754  sbcof2  1764  ax11a2  1775  ax11v  1781  sb4  1786  hbsb4t  1964  exmoeudc  2038  euimmo  2042  mopick  2053  r19.37  2558  spcimgft  2734  spcimegft  2736  rr19.28v  2796  mob2  2835  euind  2842  reuind  2860  sbeqalb  2935  triun  4007  csbexga  4024  copsexg  4134  trssord  4270  trsuc  4312  trsucss  4313  abnexg  4335  ralxfrd  4351  rexxfrd  4352  ralxfrALT  4356  sucprcreg  4432  nlimsucg  4449  tfis  4465  relssres  4825  issref  4889  dmsnopg  4978  dfco2a  5007  imadif  5171  fvelima  5439  mptfvex  5472  fvmptdf  5474  fvmptf  5479  funfvima2  5616  funfvima3  5617  foco2  5621  isores3  5682  oprabid  5769  ovmpt4g  5859  ovmpos  5860  ov2gf  5861  ovmpodf  5868  suppssfv  5944  suppssov1  5945  fo2ndf  6090  rntpos  6120  tposf2  6131  nnmordi  6378  nnmord  6379  nnaordex  6389  ectocld  6461  qsel  6472  mapsn  6550  f1oeng  6617  mapen  6706  nneneq  6717  findcard2  6749  findcard2s  6750  ac6sfi  6758  fiintim  6783  sbthlem1  6811  pr2ne  7014  ltbtwnnqq  7187  prnmaddl  7262  genpcdl  7291  genpcuu  7292  ltaddpr  7369  lteupri  7389  recexprlemss1l  7407  recexprlemss1u  7408  cauappcvgprlemdisj  7423  lttrsr  7534  recexgt0sr  7545  mulgt0sr  7550  axprecex  7652  rereceu  7661  addlsub  8096  recexap  8377  0mnnnnn0  8963  prime  9104  zeo  9110  fnn0ind  9121  zindd  9123  btwnz  9124  lbzbi  9360  addmodlteq  10122  facwordi  10437  seq3coll  10536  qdenre  10925  climcau  11067  serf0  11072  zsumdc  11104  fsum2dlemstep  11154  fsum2d  11155  fsumabs  11185  fsumiun  11197  odd2np1  11477  ndvdssub  11534  dfgcd2  11609  nprm  11711  rpexp  11738  lmss  12321  lmtopcnp  12325  txcn  12350  txlm  12354  xmettri2  12436  blin2  12507  metcnp3  12586  limcresi  12710  bj-stim  12788  bj-stan  12789  bj-stand  12790  bj-stal  12791  bj-sbimedh  12812  bj-vtoclgft  12816  elabgft1  12819  elabgf2  12821
  Copyright terms: Public domain W3C validator