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  4288  exmidundifim  4292  opth1  4323  copsexg  4331  opelopabt  4351  issod  4411  sowlin  4412  suctr  4513  reusv3i  4551  ralxfrALT  4559  ssorduni  4580  onintonm  4610  regexmidlem1  4626  nlimsucg  4659  0elnn  4712  ssrelrn  4917  issref  5114  iotaval  5293  fun11iun  5598  brprcneu  5625  fvssunirng  5647  relfvssunirn  5648  fv3  5655  ndmfvg  5663  ssimaex  5700  fvopab3ig  5713  dff4im  5786  ffnfv  5798  fconstfvm  5864  f1mpt  5904  oprabid  6042  mpoeq123  6072  f1o2ndf1  6385  brtposg  6411  rntpos  6414  dftpos4  6420  smores2  6451  tfri3  6524  rdgss  6540  nntri3or  6652  nndifsnid  6666  nnawordex  6688  eroveu  6786  map0g  6848  fundmen  6972  nneneq  7031  fiintim  7109  snon0  7118  fnfi  7119  infnlbti  7209  exmidonfinlem  7387  exmidontri2or  7444  addclpi  7530  enq0tr  7637  genprndl  7724  genprndu  7725  genpdisj  7726  addlocprlem  7738  nqprloc  7748  recexprlemss1l  7838  recexprlemss1u  7839  suplocexprlemss  7918  elrealeu  8032  ltleletr  8244  negf1o  8544  zletric  9506  zlelttric  9507  zltnle  9508  zmulcl  9516  zdcle  9539  zdclt  9540  zeo  9568  uz11  9762  indstr  9805  eqreznegel  9826  negm  9827  lbzbi  9828  fzdcel  10253  fzm1  10313  qletric  10478  qlelttric  10479  qltnle  10480  qdclt  10482  frecuzrdgtcl  10651  frecuzrdgfunlem  10658  qsqeqor  10889  swrdccatin2d  11297  rennim  11534  maxleast  11745  negfi  11760  fsum3cvg  11910  fproddccvg  12104  prodmodc  12110  ndvdssub  12462  bitsinv1lem  12493  algcvgblem  12592  algcvga  12594  isprm3  12661  oddprmdvds  12898  4sqlem2  12933  imasaddfnlemg  13368  subrngintm  14197  subrgintm  14228  lmodfopnelem1  14309  islssm  14342  lspsneq0  14411  islidlm  14464  epttop  14785  cnptoprest  14934  txcnp  14966  metequiv2  15191  cnlimcim  15366  umgrclwwlkge2  16171  bj-hbalt  16236  bj-intabssel1  16263  decidin  16270  sumdc2  16272  bj-charfunr  16282  bj-axemptylem  16364  bj-nnen2lp  16426  bj-nnord  16430  setindft  16437  bj-inf2vnlem2  16443  bj-inf2vnlem3  16444  bj-inf2vnlem4  16445  exmidsbthrlem  16504  triap  16511  tridceq  16538