Intuitionistic Logic Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  ILE Home  >  Th. List  >  syl6 GIF 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 (𝜑 → (𝜓𝜒))
syl6.2 (𝜒𝜃)
Assertion
Ref Expression
syl6 (𝜑 → (𝜓𝜃))

Proof of Theorem syl6
StepHypRef Expression
1 syl6.1 . 2 (𝜑 → (𝜓𝜒))
2 syl6.2 . . 3 (𝜒𝜃)
32a1i 9 . 2 (𝜓 → (𝜒𝜃))
41, 3sylcom 28 1 (𝜑 → (𝜓𝜃))
 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  783  con4biddc  788  dcim  818  pm3.37  822  pm2.54dc  824  pm4.79dc  843  pm2.85dc  845  pm3.12dc  900  dn1dc  902  3jao  1233  xoranor  1309  syl6an  1364  syl10  1365  hbald  1421  ax-12  1443  hbimd  1506  19.21ht  1514  19.30dc  1559  19.23t  1608  hbexd  1625  spimth  1665  spimed  1670  cbv2h  1676  equvini  1683  sbiedh  1712  sbcof2  1733  aev  1735  sb3  1754  hbsb2  1759  sbequilem  1761  sbft  1771  sbi1v  1814  cbvexdh  1844  mo23  1984  moexexdc  2027  euexex  2028  exists2  2040  dvelimdc  2242  rsp2  2418  rgen2a  2422  spcimgft  2683  spcimegft  2685  eueq3dc  2775  moeq3dc  2777  reu6  2790  ssddif  3214  reupick2  3266  sssnm  3566  prneimg  3586  dfiun2g  3730  opth1  4019  copsexg  4027  opelopabt  4045  issod  4102  sowlin  4103  suctr  4204  reusv3i  4237  ralxfrALT  4245  ssorduni  4259  onintonm  4289  regexmidlem1  4304  nlimsucg  4337  0elnn  4386  issref  4757  iotaval  4928  fun11iun  5198  brprcneu  5222  fvssunirng  5241  relfvssunirn  5242  fv3  5249  ndmfvg  5256  ssimaex  5286  fvopab3ig  5298  dff4im  5365  ffnfv  5375  fconstfvm  5431  f1mpt  5462  oprabid  5588  mpt2eq123  5615  f1o2ndf1  5900  brtposg  5923  rntpos  5926  dftpos4  5932  smores2  5963  tfri3  6036  rdgss  6052  nntri3or  6157  nndifsnid  6167  nnawordex  6188  eroveu  6284  fundmen  6374  nneneq  6413  snon0  6477  fnfi  6478  infnlbti  6533  addclpi  6631  enq0tr  6738  genprndl  6825  genprndu  6826  genpdisj  6827  addlocprlem  6839  nqprloc  6849  recexprlemss1l  6939  recexprlemss1u  6940  elrealeu  7112  ltleletr  7312  negf1o  7605  zletric  8528  zlelttric  8529  zltnle  8530  zmulcl  8537  zdcle  8557  zdclt  8558  zeo  8585  uz11  8774  indstr  8814  eqreznegel  8832  negm  8833  lbzbi  8834  fzdcel  9187  fzm1  9245  qletric  9382  qlelttric  9383  qltnle  9384  frecuzrdgtcl  9546  frecuzrdgfunlem  9553  rennim  10089  maxleast  10300  negfi  10311  fisumcvg  10401  ndvdssub  10537  algcvgblem  10638  ialgcvga  10640  isprm3  10707  bj-hbalt  10834  bj-intabssel1  10860  decidin  10867  sumdc2  10869  bj-axemptylem  10950  bj-nnen2lp  11016  bj-nnord  11020  setindft  11027  bj-inf2vnlem2  11033  bj-inf2vnlem3  11034  bj-inf2vnlem4  11035
 Copyright terms: Public domain W3C validator