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  696  pm5.21ndd  713  pm2.37  813  pm2.81  819  dcim  849  condcOLD  862  con4biddc  865  pm2.54dc  899  pm4.79dc  911  pm2.85dc  913  pm3.12dc  967  dn1dc  969  3jao  1338  xoranor  1422  syl6an  1479  syl10  1480  hbald  1540  ax12  1561  hbimd  1622  nfal  1625  19.21ht  1630  19.30dc  1676  19.23t  1725  hbexd  1742  spimth  1784  spimed  1789  cbv2h  1797  cbv2w  1799  equvini  1807  sbiedh  1836  sbcof2  1859  aev  1861  sb3  1880  hbsb2  1885  sbequilem  1887  sbft  1897  sbi1v  1942  cbvexdh  1978  nf5-1  2080  mo23  2124  moexexdc  2167  euexex  2168  exists2  2180  dvelimdc  2407  rsp2  2594  rgen2a  2598  spcimgft  2895  spcimegft  2897  eueq3dc  2994  moeq3dc  2996  reu6  3009  ssddif  3459  reupick2  3511  ifnebibdc  3672  sssnm  3863  prneimg  3883  dfiun2g  4028  exmidsssnc  4321  exmidundifim  4325  opth1  4357  copsexg  4365  opelopabt  4385  issod  4445  sowlin  4446  suctr  4547  reusv3i  4585  ralxfrALT  4593  ssorduni  4614  onintonm  4644  regexmidlem1  4660  nlimsucg  4693  0elnn  4746  ssrelrn  4952  issref  5150  iotaval  5329  fun11iun  5640  brprcneu  5668  fvssunirng  5690  relfvssunirn  5691  fv3  5698  ndmfvg  5706  ssimaex  5743  fvopab3ig  5756  dff4im  5828  ffnfv  5840  fconstfvm  5907  f1mpt  5950  oprabid  6090  mpoeq123  6120  f1o2ndf1  6437  brtposg  6498  rntpos  6501  dftpos4  6507  smores2  6538  tfri3  6611  rdgss  6627  nntri3or  6739  nndifsnid  6753  nnawordex  6775  eroveu  6873  map0g  6935  fundmen  7060  nneneq  7124  fiintim  7204  snon0  7215  fnfi  7216  infnlbti  7330  exmidonfinlem  7509  exmidontri2or  7566  addclpi  7658  enq0tr  7765  genprndl  7852  genprndu  7853  genpdisj  7854  addlocprlem  7866  nqprloc  7876  recexprlemss1l  7966  recexprlemss1u  7967  suplocexprlemss  8046  elrealeu  8160  ltleletr  8371  negf1o  8673  zletric  9641  zlelttric  9642  zltnle  9643  zmulcl  9651  zdcle  9674  zdclt  9675  zeo  9704  uz11  9898  indstr  9946  eqreznegel  9967  negm  9968  lbzbi  9969  fzdcel  10397  fzm1  10459  qletric  10628  qlelttric  10629  qltnle  10630  qdclt  10632  frecuzrdgtcl  10801  frecuzrdgfunlem  10808  qsqeqor  11039  swrdccatin2d  11464  rennim  11715  maxleast  11926  negfi  11941  fsum3cvg  12092  fproddccvg  12286  prodmodc  12292  ndvdssub  12644  bitsinv1lem  12675  algcvgblem  12774  algcvga  12776  isprm3  12843  oddprmdvds  13080  4sqlem2  13115  ballotfilemfc0  13179  ballotfilemfcc  13180  imasaddfnlemg  13581  subrngintm  14461  subrgintm  14492  lmodfopnelem1  14601  islssm  14634  lspsneq0  14703  islidlm  14756  epttop  15084  cnptoprest  15233  txcnp  15265  metequiv2  15490  cnlimcim  15665  umgrclwwlkge2  16526  bj-hbalt  16674  bj-intabssel1  16701  decidin  16708  sumdc2  16710  bj-charfunr  16719  bj-axemptylem  16801  bj-nnen2lp  16863  bj-nnord  16867  setindft  16874  bj-inf2vnlem2  16880  bj-inf2vnlem3  16881  bj-inf2vnlem4  16882  exmidsbthrlem  16941  triap  16952  tridceq  16980