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  276  adantrd  277  impel  278  mpan9  279  nsyli  623  pm2.36  778  pm4.72  797  const  822  pm2.18dc  825  con1dc  826  jadc  833  pm2.521dcALT  840  con1biimdc  843  condandc  851  pm5.18dc  853  pm2.68dc  864  annimdc  906  syl3an2  1235  syl2an23an  1262  xor3dc  1350  alrimdh  1440  spsd  1503  a5i  1507  19.21h  1521  hbnt  1616  hbae  1681  sbiedh  1745  exdistrfor  1756  sbcof2  1766  ax11a2  1777  ax11v  1783  sb4  1788  hbsb4t  1966  exmoeudc  2040  euimmo  2044  mopick  2055  r19.37  2560  spcimgft  2736  spcimegft  2738  rr19.28v  2798  mob2  2837  euind  2844  reuind  2862  sbeqalb  2937  triun  4009  csbexga  4026  copsexg  4136  trssord  4272  trsuc  4314  trsucss  4315  abnexg  4337  ralxfrd  4353  rexxfrd  4354  ralxfrALT  4358  sucprcreg  4434  nlimsucg  4451  tfis  4467  relssres  4827  issref  4891  dmsnopg  4980  dfco2a  5009  imadif  5173  fvelima  5441  mptfvex  5474  fvmptdf  5476  fvmptf  5481  funfvima2  5618  funfvima3  5619  foco2  5623  isores3  5684  oprabid  5771  ovmpt4g  5861  ovmpos  5862  ov2gf  5863  ovmpodf  5870  suppssfv  5946  suppssov1  5947  fo2ndf  6092  rntpos  6122  tposf2  6133  nnmordi  6380  nnmord  6381  nnaordex  6391  ectocld  6463  qsel  6474  mapsn  6552  f1oeng  6619  mapen  6708  nneneq  6719  findcard2  6751  findcard2s  6752  ac6sfi  6760  fiintim  6785  sbthlem1  6813  pr2ne  7016  ltbtwnnqq  7191  prnmaddl  7266  genpcdl  7295  genpcuu  7296  ltaddpr  7373  lteupri  7393  recexprlemss1l  7411  recexprlemss1u  7412  cauappcvgprlemdisj  7427  lttrsr  7538  recexgt0sr  7549  mulgt0sr  7554  axprecex  7656  rereceu  7665  addlsub  8100  recexap  8382  0mnnnnn0  8977  prime  9118  zeo  9124  fnn0ind  9135  zindd  9137  btwnz  9138  lbzbi  9376  addmodlteq  10139  facwordi  10454  seq3coll  10553  qdenre  10942  climcau  11084  serf0  11089  zsumdc  11121  fsum2dlemstep  11171  fsum2d  11172  fsumabs  11202  fsumiun  11214  odd2np1  11497  ndvdssub  11554  dfgcd2  11629  nprm  11731  rpexp  11758  lmss  12342  lmtopcnp  12346  txcn  12371  txlm  12375  xmettri2  12457  blin2  12528  metcnp3  12607  limcresi  12731  bj-stim  12881  bj-stan  12882  bj-stand  12883  bj-stal  12884  bj-sbimedh  12905  bj-vtoclgft  12909  elabgft1  12912  elabgf2  12914
  Copyright terms: Public domain W3C validator