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  48  syl6mpi  64  syl6c  66  com34  83  ex  114  syl6ib  160  syl6ibr  161  syl6bi  162  syl6bir  163  pm5.32d  443  con2d  596  con3d  603  expi  610  pm3.37  661  pm5.21ndd  677  pm2.37  777  pm2.81  783  dcim  809  condcOLD  822  con4biddc  825  pm2.54dc  859  pm4.79dc  871  pm2.85dc  873  pm3.12dc  925  dn1dc  927  3jao  1262  xoranor  1338  syl6an  1393  syl10  1394  hbald  1450  ax-12  1472  hbimd  1535  19.21ht  1543  19.30dc  1589  19.23t  1638  hbexd  1655  spimth  1696  spimed  1701  cbv2h  1707  equvini  1714  sbiedh  1743  sbcof2  1764  aev  1766  sb3  1785  hbsb2  1790  sbequilem  1792  sbft  1802  sbi1v  1845  cbvexdh  1876  mo23  2016  moexexdc  2059  euexex  2060  exists2  2072  dvelimdc  2275  rsp2  2456  rgen2a  2460  spcimgft  2733  spcimegft  2735  eueq3dc  2827  moeq3dc  2829  reu6  2842  ssddif  3276  reupick2  3328  sssnm  3647  prneimg  3667  dfiun2g  3811  exmidsssnc  4086  exmidundifim  4090  opth1  4118  copsexg  4126  opelopabt  4144  issod  4201  sowlin  4202  suctr  4303  reusv3i  4340  ralxfrALT  4348  ssorduni  4363  onintonm  4393  regexmidlem1  4408  nlimsucg  4441  0elnn  4492  issref  4879  iotaval  5057  fun11iun  5344  brprcneu  5368  fvssunirng  5390  relfvssunirn  5391  fv3  5398  ndmfvg  5406  ssimaex  5436  fvopab3ig  5449  dff4im  5520  ffnfv  5532  fconstfvm  5592  f1mpt  5626  oprabid  5757  mpoeq123  5784  f1o2ndf1  6079  brtposg  6105  rntpos  6108  dftpos4  6114  smores2  6145  tfri3  6218  rdgss  6234  nntri3or  6343  nndifsnid  6357  nnawordex  6378  eroveu  6474  map0g  6536  fundmen  6654  nneneq  6704  fiintim  6770  snon0  6776  fnfi  6777  infnlbti  6865  addclpi  7083  enq0tr  7190  genprndl  7277  genprndu  7278  genpdisj  7279  addlocprlem  7291  nqprloc  7301  recexprlemss1l  7391  recexprlemss1u  7392  elrealeu  7564  ltleletr  7769  negf1o  8063  zletric  9002  zlelttric  9003  zltnle  9004  zmulcl  9011  zdcle  9031  zdclt  9032  zeo  9060  uz11  9250  indstr  9290  eqreznegel  9308  negm  9309  lbzbi  9310  fzdcel  9713  fzm1  9773  qletric  9914  qlelttric  9915  qltnle  9916  frecuzrdgtcl  10078  frecuzrdgfunlem  10085  rennim  10666  maxleast  10877  negfi  10891  fsum3cvg  11038  ndvdssub  11475  algcvgblem  11576  algcvga  11578  isprm3  11645  epttop  12102  cnptoprest  12250  txcnp  12282  metequiv2  12485  cnlimcim  12596  bj-hbalt  12663  bj-intabssel1  12689  decidin  12696  sumdc2  12698  bj-axemptylem  12782  bj-nnen2lp  12844  bj-nnord  12848  setindft  12855  bj-inf2vnlem2  12861  bj-inf2vnlem3  12862  bj-inf2vnlem4  12863  exmidsbthrlem  12909  triap  12916