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  710  pm2.37  810  pm2.81  816  dcim  846  condcOLD  859  con4biddc  862  pm2.54dc  896  pm4.79dc  908  pm2.85dc  910  pm3.12dc  964  dn1dc  966  3jao  1335  xoranor  1419  syl6an  1476  syl10  1477  hbald  1537  ax12  1558  hbimd  1619  nfal  1622  19.21ht  1627  19.30dc  1673  19.23t  1723  hbexd  1740  spimth  1781  spimed  1786  cbv2h  1794  cbv2w  1796  equvini  1804  sbiedh  1833  sbcof2  1856  aev  1858  sb3  1877  hbsb2  1882  sbequilem  1884  sbft  1894  sbi1v  1938  cbvexdh  1973  nf5-1  2075  mo23  2119  moexexdc  2162  euexex  2163  exists2  2175  dvelimdc  2393  rsp2  2580  rgen2a  2584  spcimgft  2880  spcimegft  2882  eueq3dc  2978  moeq3dc  2980  reu6  2993  ssddif  3439  reupick2  3491  ifnebibdc  3649  sssnm  3835  prneimg  3855  dfiun2g  4000  exmidsssnc  4291  exmidundifim  4295  opth1  4326  copsexg  4334  opelopabt  4354  issod  4414  sowlin  4415  suctr  4516  reusv3i  4554  ralxfrALT  4562  ssorduni  4583  onintonm  4613  regexmidlem1  4629  nlimsucg  4662  0elnn  4715  ssrelrn  4920  issref  5117  iotaval  5296  fun11iun  5601  brprcneu  5628  fvssunirng  5650  relfvssunirn  5651  fv3  5658  ndmfvg  5666  ssimaex  5703  fvopab3ig  5716  dff4im  5789  ffnfv  5801  fconstfvm  5867  f1mpt  5907  oprabid  6045  mpoeq123  6075  f1o2ndf1  6388  brtposg  6415  rntpos  6418  dftpos4  6424  smores2  6455  tfri3  6528  rdgss  6544  nntri3or  6656  nndifsnid  6670  nnawordex  6692  eroveu  6790  map0g  6852  fundmen  6976  nneneq  7038  fiintim  7118  snon0  7128  fnfi  7129  infnlbti  7219  exmidonfinlem  7397  exmidontri2or  7454  addclpi  7540  enq0tr  7647  genprndl  7734  genprndu  7735  genpdisj  7736  addlocprlem  7748  nqprloc  7758  recexprlemss1l  7848  recexprlemss1u  7849  suplocexprlemss  7928  elrealeu  8042  ltleletr  8254  negf1o  8554  zletric  9516  zlelttric  9517  zltnle  9518  zmulcl  9526  zdcle  9549  zdclt  9550  zeo  9578  uz11  9772  indstr  9820  eqreznegel  9841  negm  9842  lbzbi  9843  fzdcel  10268  fzm1  10328  qletric  10494  qlelttric  10495  qltnle  10496  qdclt  10498  frecuzrdgtcl  10667  frecuzrdgfunlem  10674  qsqeqor  10905  swrdccatin2d  11318  rennim  11556  maxleast  11767  negfi  11782  fsum3cvg  11932  fproddccvg  12126  prodmodc  12132  ndvdssub  12484  bitsinv1lem  12515  algcvgblem  12614  algcvga  12616  isprm3  12683  oddprmdvds  12920  4sqlem2  12955  imasaddfnlemg  13390  subrngintm  14219  subrgintm  14250  lmodfopnelem1  14331  islssm  14364  lspsneq0  14433  islidlm  14486  epttop  14807  cnptoprest  14956  txcnp  14988  metequiv2  15213  cnlimcim  15388  umgrclwwlkge2  16211  bj-hbalt  16309  bj-intabssel1  16336  decidin  16343  sumdc2  16345  bj-charfunr  16355  bj-axemptylem  16437  bj-nnen2lp  16499  bj-nnord  16503  setindft  16510  bj-inf2vnlem2  16516  bj-inf2vnlem3  16517  bj-inf2vnlem4  16518  exmidsbthrlem  16576  triap  16583  tridceq  16610