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  438  con2d  587  con3d  594  expi  600  pm5.21ndd  654  pm2.37  752  pm2.81  758  condc  785  con4biddc  790  dcim  820  pm3.37  824  pm2.54dc  826  pm4.79dc  845  pm2.85dc  847  pm3.12dc  902  dn1dc  904  3jao  1235  xoranor  1311  syl6an  1366  syl10  1367  hbald  1423  ax-12  1445  hbimd  1508  19.21ht  1516  19.30dc  1561  19.23t  1610  hbexd  1627  spimth  1667  spimed  1672  cbv2h  1678  equvini  1685  sbiedh  1714  sbcof2  1735  aev  1737  sb3  1756  hbsb2  1761  sbequilem  1763  sbft  1773  sbi1v  1816  cbvexdh  1846  mo23  1986  moexexdc  2029  euexex  2030  exists2  2042  dvelimdc  2244  rsp2  2421  rgen2a  2425  spcimgft  2688  spcimegft  2690  eueq3dc  2780  moeq3dc  2782  reu6  2795  ssddif  3222  reupick2  3274  sssnm  3581  prneimg  3601  dfiun2g  3745  opth1  4037  copsexg  4045  opelopabt  4063  issod  4120  sowlin  4121  suctr  4222  reusv3i  4255  ralxfrALT  4263  ssorduni  4277  onintonm  4307  regexmidlem1  4322  nlimsucg  4355  0elnn  4405  issref  4781  iotaval  4957  fun11iun  5237  brprcneu  5261  fvssunirng  5283  relfvssunirn  5284  fv3  5291  ndmfvg  5298  ssimaex  5328  fvopab3ig  5341  dff4im  5408  ffnfv  5419  fconstfvm  5476  f1mpt  5511  oprabid  5638  mpt2eq123  5665  f1o2ndf1  5950  brtposg  5973  rntpos  5976  dftpos4  5982  smores2  6013  tfri3  6086  rdgss  6102  nntri3or  6208  nndifsnid  6218  nnawordex  6239  eroveu  6335  map0g  6397  fundmen  6475  nneneq  6525  snon0  6595  fnfi  6596  infnlbti  6665  addclpi  6830  enq0tr  6937  genprndl  7024  genprndu  7025  genpdisj  7026  addlocprlem  7038  nqprloc  7048  recexprlemss1l  7138  recexprlemss1u  7139  elrealeu  7311  ltleletr  7511  negf1o  7804  zletric  8727  zlelttric  8728  zltnle  8729  zmulcl  8736  zdcle  8756  zdclt  8757  zeo  8784  uz11  8973  indstr  9013  eqreznegel  9031  negm  9032  lbzbi  9033  fzdcel  9386  fzm1  9444  qletric  9583  qlelttric  9584  qltnle  9585  frecuzrdgtcl  9747  frecuzrdgfunlem  9754  rennim  10331  maxleast  10542  negfi  10554  fisumcvg  10658  ndvdssub  10812  algcvgblem  10913  ialgcvga  10915  isprm3  10982  bj-hbalt  11109  bj-intabssel1  11135  decidin  11142  sumdc2  11144  bj-axemptylem  11228  bj-nnen2lp  11294  bj-nnord  11298  setindft  11305  bj-inf2vnlem2  11311  bj-inf2vnlem3  11312  bj-inf2vnlem4  11313  exmidsbthrlem  11357