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  46  syl6mpi  62  syl6c  64  com34  81  ex  112  syl6ib  154  syl6ibr  155  syl6bi  156  syl6bir  157  pm5.32d  431  con2d  564  con3d  571  expi  577  pm5.21ndd  631  pm2.37  729  pm2.81  735  condc  760  con4biddc  765  dcim  795  pm3.37  799  pm2.54dc  801  pm4.79dc  820  pm2.85dc  822  pm3.12dc  876  dn1dc  878  3jao  1207  xoranor  1284  syl6an  1339  syl10  1340  hbald  1396  ax-12  1418  hbimd  1481  19.21ht  1489  19.30dc  1534  19.23t  1583  hbexd  1600  spimth  1639  spimed  1644  cbv2h  1650  equvini  1657  sbiedh  1686  sbcof2  1707  aev  1709  sb3  1728  hbsb2  1733  sbequilem  1735  sbft  1744  sbi1v  1787  cbvexdh  1817  mo23  1957  moexexdc  2000  euexex  2001  exists2  2013  dvelimdc  2213  rsp2  2388  rgen2a  2392  spcimgft  2646  spcimegft  2648  eueq3dc  2738  moeq3dc  2740  reu6  2753  ssddif  3199  reupick2  3251  sssnm  3553  prneimg  3573  dfiun2g  3717  opth1  4001  copsexg  4009  opelopabt  4027  issod  4084  sowlin  4085  suctr  4186  reusv3i  4219  ralxfrALT  4227  ssorduni  4241  onintonm  4271  regexmidlem1  4286  nlimsucg  4318  0elnn  4368  issref  4735  iotaval  4906  fun11iun  5175  brprcneu  5199  fvssunirng  5218  relfvssunirn  5219  fv3  5225  ndmfvg  5232  ssimaex  5262  fvopab3ig  5274  dff4im  5341  ffnfv  5351  fconstfvm  5407  f1mpt  5438  oprabid  5565  mpt2eq123  5592  f1o2ndf1  5877  brtposg  5900  rntpos  5903  dftpos4  5909  smores2  5940  tfr0  5968  tfri3  5984  rdgss  6001  rdgon  6004  nntri3or  6103  nnawordex  6132  eroveu  6228  fundmen  6317  nneneq  6351  snon0  6387  addclpi  6483  enq0tr  6590  genprndl  6677  genprndu  6678  genpdisj  6679  addlocprlem  6691  nqprloc  6701  recexprlemss1l  6791  recexprlemss1u  6792  elrealeu  6964  ltleletr  7159  zletric  8346  zlelttric  8347  zltnle  8348  zmulcl  8355  zdcle  8375  zdclt  8376  zeo  8402  uz11  8591  indstr  8632  eqreznegel  8646  negm  8647  lbzbi  8648  fzdcel  9006  fzm1  9064  qletric  9201  qlelttric  9202  qltnle  9203  frecuzrdgfn  9362  rennim  9829  ndvdssub  10242  algcvgblem  10271  ialgcvga  10273  bj-hbalt  10290  bj-intabssel1  10316  bj-axemptylem  10399  bj-nnen2lp  10466  bj-nnord  10470  setindft  10477  bj-inf2vnlem2  10483  bj-inf2vnlem3  10484  bj-inf2vnlem4  10485
  Copyright terms: Public domain W3C validator