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-mp 5  ax-1 6  ax-2 7
This theorem is referenced by:  syl56  34  syl6com  35  a1dd  48  syl6mpi  64  syl6c  66  com34  83  ex  114  syl6ib  160  syl6ibr  161  syl6bi  162  syl6bir  163  pm5.32d  443  con2d  596  con3d  603  expi  610  pm3.37  661  pm5.21ndd  677  pm2.37  777  pm2.81  783  dcim  809  condcOLD  822  con4biddc  825  pm2.54dc  859  pm4.79dc  871  pm2.85dc  873  pm3.12dc  925  dn1dc  927  3jao  1262  xoranor  1338  syl6an  1393  syl10  1394  hbald  1450  ax-12  1472  hbimd  1535  19.21ht  1543  19.30dc  1589  19.23t  1638  hbexd  1655  spimth  1696  spimed  1701  cbv2h  1707  equvini  1714  sbiedh  1743  sbcof2  1764  aev  1766  sb3  1785  hbsb2  1790  sbequilem  1792  sbft  1802  sbi1v  1845  cbvexdh  1876  mo23  2016  moexexdc  2059  euexex  2060  exists2  2072  dvelimdc  2276  rsp2  2457  rgen2a  2461  spcimgft  2734  spcimegft  2736  eueq3dc  2829  moeq3dc  2831  reu6  2844  ssddif  3278  reupick2  3330  sssnm  3649  prneimg  3669  dfiun2g  3813  exmidsssnc  4094  exmidundifim  4098  opth1  4126  copsexg  4134  opelopabt  4152  issod  4209  sowlin  4210  suctr  4311  reusv3i  4348  ralxfrALT  4356  ssorduni  4371  onintonm  4401  regexmidlem1  4416  nlimsucg  4449  0elnn  4500  issref  4889  iotaval  5067  fun11iun  5354  brprcneu  5380  fvssunirng  5402  relfvssunirn  5403  fv3  5410  ndmfvg  5418  ssimaex  5448  fvopab3ig  5461  dff4im  5532  ffnfv  5544  fconstfvm  5604  f1mpt  5638  oprabid  5769  mpoeq123  5796  f1o2ndf1  6091  brtposg  6117  rntpos  6120  dftpos4  6126  smores2  6157  tfri3  6230  rdgss  6246  nntri3or  6355  nndifsnid  6369  nnawordex  6390  eroveu  6486  map0g  6548  fundmen  6666  nneneq  6717  fiintim  6783  snon0  6790  fnfi  6791  infnlbti  6879  addclpi  7099  enq0tr  7206  genprndl  7293  genprndu  7294  genpdisj  7295  addlocprlem  7307  nqprloc  7317  recexprlemss1l  7407  recexprlemss1u  7408  suplocexprlemss  7487  elrealeu  7601  ltleletr  7810  negf1o  8108  zletric  9052  zlelttric  9053  zltnle  9054  zmulcl  9061  zdcle  9081  zdclt  9082  zeo  9110  uz11  9300  indstr  9340  eqreznegel  9358  negm  9359  lbzbi  9360  fzdcel  9771  fzm1  9831  qletric  9972  qlelttric  9973  qltnle  9974  frecuzrdgtcl  10136  frecuzrdgfunlem  10143  rennim  10725  maxleast  10936  negfi  10950  fsum3cvg  11097  ndvdssub  11534  algcvgblem  11637  algcvga  11639  isprm3  11706  epttop  12165  cnptoprest  12314  txcnp  12346  metequiv2  12571  cnlimcim  12715  bj-hbalt  12804  bj-intabssel1  12831  decidin  12838  sumdc2  12840  bj-axemptylem  12924  bj-nnen2lp  12986  bj-nnord  12990  setindft  12997  bj-inf2vnlem2  13003  bj-inf2vnlem3  13004  bj-inf2vnlem4  13005  exmidsbthrlem  13051  triap  13058
  Copyright terms: Public domain W3C validator