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-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  446  con2d  614  con3d  621  expi  628  pm3.37  679  pm5.21ndd  695  pm2.37  795  pm2.81  801  dcim  827  condcOLD  840  con4biddc  843  pm2.54dc  877  pm4.79dc  889  pm2.85dc  891  pm3.12dc  943  dn1dc  945  3jao  1280  xoranor  1356  syl6an  1411  syl10  1412  hbald  1468  ax-12  1490  hbimd  1553  19.21ht  1561  19.30dc  1607  19.23t  1656  hbexd  1673  spimth  1714  spimed  1719  cbv2h  1725  equvini  1732  sbiedh  1761  sbcof2  1783  aev  1785  sb3  1804  hbsb2  1809  sbequilem  1811  sbft  1821  sbi1v  1864  cbvexdh  1899  mo23  2041  moexexdc  2084  euexex  2085  exists2  2097  dvelimdc  2302  rsp2  2486  rgen2a  2490  spcimgft  2766  spcimegft  2768  eueq3dc  2863  moeq3dc  2865  reu6  2878  ssddif  3316  reupick2  3368  sssnm  3690  prneimg  3710  dfiun2g  3854  exmidsssnc  4136  exmidundifim  4140  opth1  4168  copsexg  4176  opelopabt  4194  issod  4251  sowlin  4252  suctr  4353  reusv3i  4390  ralxfrALT  4398  ssorduni  4413  onintonm  4443  regexmidlem1  4458  nlimsucg  4491  0elnn  4543  issref  4932  iotaval  5110  fun11iun  5399  brprcneu  5425  fvssunirng  5447  relfvssunirn  5448  fv3  5455  ndmfvg  5463  ssimaex  5493  fvopab3ig  5506  dff4im  5577  ffnfv  5589  fconstfvm  5649  f1mpt  5683  oprabid  5814  mpoeq123  5841  f1o2ndf1  6136  brtposg  6162  rntpos  6165  dftpos4  6171  smores2  6202  tfri3  6275  rdgss  6291  nntri3or  6400  nndifsnid  6414  nnawordex  6435  eroveu  6531  map0g  6593  fundmen  6711  nneneq  6762  fiintim  6833  snon0  6840  fnfi  6841  infnlbti  6929  exmidonfinlem  7076  onntri52  7120  addclpi  7186  enq0tr  7293  genprndl  7380  genprndu  7381  genpdisj  7382  addlocprlem  7394  nqprloc  7404  recexprlemss1l  7494  recexprlemss1u  7495  suplocexprlemss  7574  elrealeu  7688  ltleletr  7897  negf1o  8195  zletric  9149  zlelttric  9150  zltnle  9151  zmulcl  9158  zdcle  9178  zdclt  9179  zeo  9207  uz11  9399  indstr  9442  eqreznegel  9460  negm  9461  lbzbi  9462  fzdcel  9878  fzm1  9938  qletric  10079  qlelttric  10080  qltnle  10081  frecuzrdgtcl  10243  frecuzrdgfunlem  10250  rennim  10833  maxleast  11044  negfi  11058  fsum3cvg  11206  fproddccvg  11400  prodmodc  11406  ndvdssub  11697  algcvgblem  11800  algcvga  11802  isprm3  11869  epttop  12332  cnptoprest  12481  txcnp  12513  metequiv2  12738  cnlimcim  12882  bj-hbalt  13179  bj-intabssel1  13206  decidin  13213  sumdc2  13215  bj-charfunr  13223  bj-axemptylem  13305  bj-nnen2lp  13367  bj-nnord  13371  setindft  13378  bj-inf2vnlem2  13384  bj-inf2vnlem3  13385  bj-inf2vnlem4  13386  exmidsbthrlem  13435  triap  13442  tridceq  13469
 Copyright terms: Public domain W3C validator