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  2879  spcimegft  2881  eueq3dc  2977  moeq3dc  2979  reu6  2992  ssddif  3438  reupick2  3490  ifnebibdc  3648  sssnm  3832  prneimg  3852  dfiun2g  3997  exmidsssnc  4287  exmidundifim  4291  opth1  4322  copsexg  4330  opelopabt  4350  issod  4410  sowlin  4411  suctr  4512  reusv3i  4550  ralxfrALT  4558  ssorduni  4579  onintonm  4609  regexmidlem1  4625  nlimsucg  4658  0elnn  4711  ssrelrn  4914  issref  5111  iotaval  5290  fun11iun  5595  brprcneu  5622  fvssunirng  5644  relfvssunirn  5645  fv3  5652  ndmfvg  5660  ssimaex  5697  fvopab3ig  5710  dff4im  5783  ffnfv  5795  fconstfvm  5861  f1mpt  5901  oprabid  6039  mpoeq123  6069  f1o2ndf1  6380  brtposg  6406  rntpos  6409  dftpos4  6415  smores2  6446  tfri3  6519  rdgss  6535  nntri3or  6647  nndifsnid  6661  nnawordex  6683  eroveu  6781  map0g  6843  fundmen  6967  nneneq  7026  fiintim  7101  snon0  7110  fnfi  7111  infnlbti  7201  exmidonfinlem  7379  exmidontri2or  7436  addclpi  7522  enq0tr  7629  genprndl  7716  genprndu  7717  genpdisj  7718  addlocprlem  7730  nqprloc  7740  recexprlemss1l  7830  recexprlemss1u  7831  suplocexprlemss  7910  elrealeu  8024  ltleletr  8236  negf1o  8536  zletric  9498  zlelttric  9499  zltnle  9500  zmulcl  9508  zdcle  9531  zdclt  9532  zeo  9560  uz11  9753  indstr  9796  eqreznegel  9817  negm  9818  lbzbi  9819  fzdcel  10244  fzm1  10304  qletric  10469  qlelttric  10470  qltnle  10471  qdclt  10473  frecuzrdgtcl  10642  frecuzrdgfunlem  10649  qsqeqor  10880  swrdccatin2d  11284  rennim  11521  maxleast  11732  negfi  11747  fsum3cvg  11897  fproddccvg  12091  prodmodc  12097  ndvdssub  12449  bitsinv1lem  12480  algcvgblem  12579  algcvga  12581  isprm3  12648  oddprmdvds  12885  4sqlem2  12920  imasaddfnlemg  13355  subrngintm  14184  subrgintm  14215  lmodfopnelem1  14296  islssm  14329  lspsneq0  14398  islidlm  14451  epttop  14772  cnptoprest  14921  txcnp  14953  metequiv2  15178  cnlimcim  15353  bj-hbalt  16151  bj-intabssel1  16178  decidin  16185  sumdc2  16187  bj-charfunr  16197  bj-axemptylem  16279  bj-nnen2lp  16341  bj-nnord  16345  setindft  16352  bj-inf2vnlem2  16358  bj-inf2vnlem3  16359  bj-inf2vnlem4  16360  exmidsbthrlem  16420  triap  16427  tridceq  16454