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

Step	Hyp	Ref	Expression
1		syl6.1	. 2 ⊢ (𝜑 → (𝜓 → 𝜒))
2		syl6.2	. . 3 ⊢ (𝜒 → 𝜃)
3	2	a1i 9	. 2 ⊢ (𝜓 → (𝜒 → 𝜃))
4	1, 3	sylcom 28	1 ⊢ (𝜑 → (𝜓 → 𝜃))

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  115  imbitrdi  161  imbitrrdi  162  biimtrdi  163  biimtrrdi  164  pm5.32d  450  con2d  629  con3d  636  expi  643  pm3.37  695  pm5.21ndd  712  pm2.37  812  pm2.81  818  dcim  848  condcOLD  861  con4biddc  864  pm2.54dc  898  pm4.79dc  910  pm2.85dc  912  pm3.12dc  966  dn1dc  968  3jao  1337  xoranor  1421  syl6an  1478  syl10  1479  hbald  1539  ax12  1560  hbimd  1621  nfal  1624  19.21ht  1629  19.30dc  1675  19.23t  1724  hbexd  1741  spimth  1782  spimed  1787  cbv2h  1795  cbv2w  1797  equvini  1805  sbiedh  1834  sbcof2  1857  aev  1859  sb3  1878  hbsb2  1883  sbequilem  1885  sbft  1895  sbi1v  1939  cbvexdh  1974  nf5-1  2076  mo23  2120  moexexdc  2163  euexex  2164  exists2  2176  dvelimdc  2394  rsp2  2581  rgen2a  2585  spcimgft  2881  spcimegft  2883  eueq3dc  2979  moeq3dc  2981  reu6  2994  ssddif  3440  reupick2  3492  ifnebibdc  3652  sssnm  3838  prneimg  3858  dfiun2g  4003  exmidsssnc  4295  exmidundifim  4299  opth1  4330  copsexg  4338  opelopabt  4358  issod  4418  sowlin  4419  suctr  4520  reusv3i  4558  ralxfrALT  4566  ssorduni  4587  onintonm  4617  regexmidlem1  4633  nlimsucg  4666  0elnn  4719  ssrelrn  4924  issref  5121  iotaval  5300  fun11iun  5607  brprcneu  5635  fvssunirng  5657  relfvssunirn  5658  fv3  5665  ndmfvg  5673  ssimaex  5710  fvopab3ig  5723  dff4im  5796  ffnfv  5808  fconstfvm  5875  f1mpt  5917  oprabid  6055  mpoeq123  6085  f1o2ndf1  6398  brtposg  6425  rntpos  6428  dftpos4  6434  smores2  6465  tfri3  6538  rdgss  6554  nntri3or  6666  nndifsnid  6680  nnawordex  6702  eroveu  6800  map0g  6862  fundmen  6986  nneneq  7048  fiintim  7128  snon0  7139  fnfi  7140  infnlbti  7230  exmidonfinlem  7409  exmidontri2or  7466  addclpi  7552  enq0tr  7659  genprndl  7746  genprndu  7747  genpdisj  7748  addlocprlem  7760  nqprloc  7770  recexprlemss1l  7860  recexprlemss1u  7861  suplocexprlemss  7940  elrealeu  8054  ltleletr  8266  negf1o  8566  zletric  9528  zlelttric  9529  zltnle  9530  zmulcl  9538  zdcle  9561  zdclt  9562  zeo  9590  uz11  9784  indstr  9832  eqreznegel  9853  negm  9854  lbzbi  9855  fzdcel  10280  fzm1  10340  qletric  10507  qlelttric  10508  qltnle  10509  qdclt  10511  frecuzrdgtcl  10680  frecuzrdgfunlem  10687  qsqeqor  10918  swrdccatin2d  11334  rennim  11585  maxleast  11796  negfi  11811  fsum3cvg  11962  fproddccvg  12156  prodmodc  12162  ndvdssub  12514  bitsinv1lem  12545  algcvgblem  12644  algcvga  12646  isprm3  12713  oddprmdvds  12950  4sqlem2  12985  imasaddfnlemg  13420  subrngintm  14250  subrgintm  14281  lmodfopnelem1  14362  islssm  14395  lspsneq0  14464  islidlm  14517  epttop  14843  cnptoprest  14992  txcnp  15024  metequiv2  15249  cnlimcim  15424  umgrclwwlkge2  16282  bj-hbalt  16420  bj-intabssel1  16447  decidin  16454  sumdc2  16456  bj-charfunr  16465  bj-axemptylem  16547  bj-nnen2lp  16609  bj-nnord  16613  setindft  16620  bj-inf2vnlem2  16626  bj-inf2vnlem3  16627  bj-inf2vnlem4  16628  exmidsbthrlem  16689  triap  16700  tridceq  16728