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-1 5  ax-2 6  ax-mp 7

This theorem is referenced by:  syl56  34  syl6com  35  a1dd  47  syl6mpi  63  syl6c  65  com34  82  ex  113  syl6ib  159  syl6ibr  160  syl6bi  161  syl6bir  162  pm5.32d  437  con2d  586  con3d  593  expi  599  pm5.21ndd  653  pm2.37  751  pm2.81  757  condc  782  con4biddc  787  dcim  817  pm3.37  821  pm2.54dc  823  pm4.79dc  842  pm2.85dc  844  pm3.12dc  899  dn1dc  901  3jao  1232  xoranor  1308  syl6an  1363  syl10  1364  hbald  1420  ax-12  1442  hbimd  1505  19.21ht  1513  19.30dc  1558  19.23t  1607  hbexd  1624  spimth  1663  spimed  1668  cbv2h  1674  equvini  1681  sbiedh  1710  sbcof2  1731  aev  1733  sb3  1752  hbsb2  1757  sbequilem  1759  sbft  1769  sbi1v  1812  cbvexdh  1842  mo23  1982  moexexdc  2025  euexex  2026  exists2  2038  dvelimdc  2238  rsp2  2413  rgen2a  2417  spcimgft  2674  spcimegft  2676  eueq3dc  2766  moeq3dc  2768  reu6  2781  ssddif  3198  reupick2  3250  sssnm  3546  prneimg  3566  dfiun2g  3710  opth1  3991  copsexg  3999  opelopabt  4017  issod  4074  sowlin  4075  suctr  4176  reusv3i  4209  ralxfrALT  4217  ssorduni  4231  onintonm  4261  regexmidlem1  4276  nlimsucg  4309  0elnn  4358  issref  4727  iotaval  4898  fun11iun  5167  brprcneu  5191  fvssunirng  5210  relfvssunirn  5211  fv3  5218  ndmfvg  5225  ssimaex  5255  fvopab3ig  5267  dff4im  5334  ffnfv  5344  fconstfvm  5400  f1mpt  5431  oprabid  5557  mpt2eq123  5584  f1o2ndf1  5869  brtposg  5892  rntpos  5895  dftpos4  5901  smores2  5932  tfr0  5960  tfri3  5976  rdgss  5993  rdgon  5996  nntri3or  6095  nnawordex  6124  eroveu  6220  fundmen  6309  nneneq  6343  snon0  6387  fnfi  6388  infnlbti  6439  addclpi  6517  enq0tr  6624  genprndl  6711  genprndu  6712  genpdisj  6713  addlocprlem  6725  nqprloc  6735  recexprlemss1l  6825  recexprlemss1u  6826  elrealeu  6998  ltleletr  7193  negf1o  7486  zletric  8395  zlelttric  8396  zltnle  8397  zmulcl  8404  zdcle  8424  zdclt  8425  zeo  8452  uz11  8641  indstr  8681  eqreznegel  8699  negm  8700  lbzbi  8701  fzdcel  9059  fzm1  9117  qletric  9253  qlelttric  9254  qltnle  9255  frecuzrdgfn  9414  rennim  9888  maxleast  10099  negfi  10110  ndvdssub  10330  algcvgblem  10431  ialgcvga  10433  isprm3  10500  bj-hbalt  10574  bj-intabssel1  10600  bj-axemptylem  10683  bj-nnen2lp  10749  bj-nnord  10753  setindft  10760  bj-inf2vnlem2  10766  bj-inf2vnlem3  10767  bj-inf2vnlem4  10768