ILE Home 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  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  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  2737  moeq3dc  2739  reu6  2752  ssddif  3198  reupick2  3250  sssnm  3552  prneimg  3572  dfiun2g  3716  opth1  4000  copsexg  4008  opelopabt  4026  issod  4083  sowlin  4084  suctr  4185  reusv3i  4218  ralxfrALT  4226  ssorduni  4240  onintonm  4270  regexmidlem1  4285  nlimsucg  4317  0elnn  4367  issref  4734  iotaval  4905  fun11iun  5174  brprcneu  5198  fvssunirng  5217  relfvssunirn  5218  fv3  5224  ndmfvg  5231  ssimaex  5261  fvopab3ig  5273  dff4im  5340  ffnfv  5350  fconstfvm  5406  f1mpt  5437  oprabid  5564  mpt2eq123  5591  f1o2ndf1  5876  brtposg  5899  rntpos  5902  dftpos4  5908  smores2  5939  tfr0  5967  tfri3  5983  rdgss  6000  rdgon  6003  nntri3or  6102  nnawordex  6131  eroveu  6227  fundmen  6316  nneneq  6350  snon0  6386  addclpi  6482  enq0tr  6589  genprndl  6676  genprndu  6677  genpdisj  6678  addlocprlem  6690  nqprloc  6700  recexprlemss1l  6790  recexprlemss1u  6791  elrealeu  6963  ltleletr  7158  zletric  8345  zlelttric  8346  zltnle  8347  zmulcl  8354  zdcle  8374  zdclt  8375  zeo  8401  uz11  8590  indstr  8631  eqreznegel  8645  negm  8646  lbzbi  8647  fzdcel  9005  fzm1  9063  qletric  9200  qlelttric  9201  qltnle  9202  frecuzrdgfn  9356  rennim  9821  algcvgblem  10243  ialgcvga  10245  bj-hbalt  10262  bj-intabssel1  10288  bj-axemptylem  10371  bj-nnen2lp  10438  bj-nnord  10442  setindft  10449  bj-inf2vnlem2  10455  bj-inf2vnlem3  10456  bj-inf2vnlem4  10457
  Copyright terms: Public domain W3C validator