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  627  con3d  634  expi  641  pm3.37  693  pm5.21ndd  709  pm2.37  809  pm2.81  815  dcim  845  condcOLD  858  con4biddc  861  pm2.54dc  895  pm4.79dc  907  pm2.85dc  909  pm3.12dc  963  dn1dc  965  3jao  1316  xoranor  1399  syl6an  1456  syl10  1457  hbald  1517  ax12  1538  hbimd  1599  nfal  1602  19.21ht  1607  19.30dc  1653  19.23t  1703  hbexd  1720  spimth  1761  spimed  1766  cbv2h  1774  cbv2w  1776  equvini  1784  sbiedh  1813  sbcof2  1836  aev  1838  sb3  1857  hbsb2  1862  sbequilem  1864  sbft  1874  sbi1v  1918  cbvexdh  1953  nf5-1  2055  mo23  2099  moexexdc  2142  euexex  2143  exists2  2155  dvelimdc  2373  rsp2  2560  rgen2a  2564  spcimgft  2859  spcimegft  2861  eueq3dc  2957  moeq3dc  2959  reu6  2972  ssddif  3418  reupick2  3470  ifnebibdc  3628  sssnm  3811  prneimg  3831  dfiun2g  3976  exmidsssnc  4266  exmidundifim  4270  opth1  4301  copsexg  4309  opelopabt  4329  issod  4387  sowlin  4388  suctr  4489  reusv3i  4527  ralxfrALT  4535  ssorduni  4556  onintonm  4586  regexmidlem1  4602  nlimsucg  4635  0elnn  4688  ssrelrn  4891  issref  5087  iotaval  5266  fun11iun  5569  brprcneu  5596  fvssunirng  5618  relfvssunirn  5619  fv3  5626  ndmfvg  5634  ssimaex  5668  fvopab3ig  5681  dff4im  5754  ffnfv  5766  fconstfvm  5830  f1mpt  5868  oprabid  6006  mpoeq123  6034  f1o2ndf1  6344  brtposg  6370  rntpos  6373  dftpos4  6379  smores2  6410  tfri3  6483  rdgss  6499  nntri3or  6609  nndifsnid  6623  nnawordex  6645  eroveu  6743  map0g  6805  fundmen  6929  nneneq  6986  fiintim  7061  snon0  7070  fnfi  7071  infnlbti  7161  exmidonfinlem  7339  exmidontri2or  7396  addclpi  7482  enq0tr  7589  genprndl  7676  genprndu  7677  genpdisj  7678  addlocprlem  7690  nqprloc  7700  recexprlemss1l  7790  recexprlemss1u  7791  suplocexprlemss  7870  elrealeu  7984  ltleletr  8196  negf1o  8496  zletric  9458  zlelttric  9459  zltnle  9460  zmulcl  9468  zdcle  9491  zdclt  9492  zeo  9520  uz11  9713  indstr  9756  eqreznegel  9777  negm  9778  lbzbi  9779  fzdcel  10204  fzm1  10264  qletric  10428  qlelttric  10429  qltnle  10430  qdclt  10432  frecuzrdgtcl  10601  frecuzrdgfunlem  10608  qsqeqor  10839  swrdccatin2d  11242  rennim  11479  maxleast  11690  negfi  11705  fsum3cvg  11855  fproddccvg  12049  prodmodc  12055  ndvdssub  12407  bitsinv1lem  12438  algcvgblem  12537  algcvga  12539  isprm3  12606  oddprmdvds  12843  4sqlem2  12878  imasaddfnlemg  13313  subrngintm  14141  subrgintm  14172  lmodfopnelem1  14253  islssm  14286  lspsneq0  14355  islidlm  14408  epttop  14729  cnptoprest  14878  txcnp  14910  metequiv2  15135  cnlimcim  15310  bj-hbalt  16037  bj-intabssel1  16064  decidin  16071  sumdc2  16073  bj-charfunr  16083  bj-axemptylem  16165  bj-nnen2lp  16227  bj-nnord  16231  setindft  16238  bj-inf2vnlem2  16244  bj-inf2vnlem3  16245  bj-inf2vnlem4  16246  exmidsbthrlem  16301  triap  16308  tridceq  16335