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

Theorem syl6 33
Description: A syllogism rule of inference. The second premise is used to replace the consequent of the first premise. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 30-Jul-2012.)
Hypotheses
Ref Expression
syl6.1  |-  ( ph  ->  ( ps  ->  ch ) )
syl6.2  |-  ( ch 
->  th )
Assertion
Ref Expression
syl6  |-  ( ph  ->  ( ps  ->  th )
)

Proof of Theorem syl6
StepHypRef Expression
1 syl6.1 . 2  |-  ( ph  ->  ( ps  ->  ch ) )
2 syl6.2 . . 3  |-  ( ch 
->  th )
32a1i 9 . 2  |-  ( ps 
->  ( ch  ->  th )
)
41, 3sylcom 28 1  |-  ( ph  ->  ( ps  ->  th )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7
This theorem is referenced by:  syl56  34  syl6com  35  a1dd  47  syl6mpi  63  syl6c  65  com34  82  ex  113  syl6ib  159  syl6ibr  160  syl6bi  161  syl6bir  162  pm5.32d  438  con2d  587  con3d  594  expi  600  pm5.21ndd  654  pm2.37  752  pm2.81  758  condc  785  con4biddc  790  dcim  820  pm3.37  824  pm2.54dc  826  pm4.79dc  845  pm2.85dc  847  pm3.12dc  902  dn1dc  904  3jao  1235  xoranor  1311  syl6an  1366  syl10  1367  hbald  1423  ax-12  1445  hbimd  1508  19.21ht  1516  19.30dc  1561  19.23t  1610  hbexd  1627  spimth  1667  spimed  1672  cbv2h  1678  equvini  1685  sbiedh  1714  sbcof2  1735  aev  1737  sb3  1756  hbsb2  1761  sbequilem  1763  sbft  1773  sbi1v  1816  cbvexdh  1846  mo23  1986  moexexdc  2029  euexex  2030  exists2  2042  dvelimdc  2244  rsp2  2421  rgen2a  2425  spcimgft  2688  spcimegft  2690  eueq3dc  2780  moeq3dc  2782  reu6  2795  ssddif  3222  reupick2  3274  sssnm  3583  prneimg  3603  dfiun2g  3747  opth1  4039  copsexg  4047  opelopabt  4065  issod  4122  sowlin  4123  suctr  4224  reusv3i  4257  ralxfrALT  4265  ssorduni  4279  onintonm  4309  regexmidlem1  4324  nlimsucg  4357  0elnn  4407  issref  4783  iotaval  4959  fun11iun  5239  brprcneu  5263  fvssunirng  5285  relfvssunirn  5286  fv3  5293  ndmfvg  5300  ssimaex  5330  fvopab3ig  5343  dff4im  5410  ffnfv  5421  fconstfvm  5478  f1mpt  5513  oprabid  5640  mpt2eq123  5667  f1o2ndf1  5952  brtposg  5975  rntpos  5978  dftpos4  5984  smores2  6015  tfri3  6088  rdgss  6104  nntri3or  6210  nndifsnid  6220  nnawordex  6241  eroveu  6337  map0g  6399  fundmen  6477  nneneq  6527  snon0  6598  fnfi  6599  infnlbti  6668  addclpi  6833  enq0tr  6940  genprndl  7027  genprndu  7028  genpdisj  7029  addlocprlem  7041  nqprloc  7051  recexprlemss1l  7141  recexprlemss1u  7142  elrealeu  7314  ltleletr  7514  negf1o  7807  zletric  8730  zlelttric  8731  zltnle  8732  zmulcl  8739  zdcle  8759  zdclt  8760  zeo  8787  uz11  8976  indstr  9016  eqreznegel  9034  negm  9035  lbzbi  9036  fzdcel  9389  fzm1  9447  qletric  9586  qlelttric  9587  qltnle  9588  frecuzrdgtcl  9750  frecuzrdgfunlem  9757  rennim  10352  maxleast  10563  negfi  10575  fisumcvg  10680  ndvdssub  10855  algcvgblem  10956  ialgcvga  10958  isprm3  11025  bj-hbalt  11152  bj-intabssel1  11178  decidin  11185  sumdc2  11187  bj-axemptylem  11271  bj-nnen2lp  11337  bj-nnord  11341  setindft  11348  bj-inf2vnlem2  11354  bj-inf2vnlem3  11355  bj-inf2vnlem4  11356  exmidsbthrlem  11400
  Copyright terms: Public domain W3C validator