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  625  con3d  632  expi  639  pm3.37  690  pm5.21ndd  706  pm2.37  806  pm2.81  812  dcim  842  condcOLD  855  con4biddc  858  pm2.54dc  892  pm4.79dc  904  pm2.85dc  906  pm3.12dc  960  dn1dc  962  3jao  1312  xoranor  1388  syl6an  1445  syl10  1446  hbald  1505  ax12  1526  hbimd  1587  nfal  1590  19.21ht  1595  19.30dc  1641  19.23t  1691  hbexd  1708  spimth  1749  spimed  1754  cbv2h  1762  cbv2w  1764  equvini  1772  sbiedh  1801  sbcof2  1824  aev  1826  sb3  1845  hbsb2  1850  sbequilem  1852  sbft  1862  sbi1v  1906  cbvexdh  1941  nf5-1  2043  mo23  2086  moexexdc  2129  euexex  2130  exists2  2142  dvelimdc  2360  rsp2  2547  rgen2a  2551  spcimgft  2840  spcimegft  2842  eueq3dc  2938  moeq3dc  2940  reu6  2953  ssddif  3398  reupick2  3450  ifnebibdc  3605  sssnm  3785  prneimg  3805  dfiun2g  3949  exmidsssnc  4237  exmidundifim  4241  opth1  4270  copsexg  4278  opelopabt  4297  issod  4355  sowlin  4356  suctr  4457  reusv3i  4495  ralxfrALT  4503  ssorduni  4524  onintonm  4554  regexmidlem1  4570  nlimsucg  4603  0elnn  4656  issref  5053  iotaval  5231  fun11iun  5528  brprcneu  5554  fvssunirng  5576  relfvssunirn  5577  fv3  5584  ndmfvg  5592  ssimaex  5625  fvopab3ig  5638  dff4im  5711  ffnfv  5723  fconstfvm  5783  f1mpt  5821  oprabid  5957  mpoeq123  5985  f1o2ndf1  6295  brtposg  6321  rntpos  6324  dftpos4  6330  smores2  6361  tfri3  6434  rdgss  6450  nntri3or  6560  nndifsnid  6574  nnawordex  6596  eroveu  6694  map0g  6756  fundmen  6874  nneneq  6927  fiintim  7001  snon0  7010  fnfi  7011  infnlbti  7101  exmidonfinlem  7272  exmidontri2or  7326  addclpi  7411  enq0tr  7518  genprndl  7605  genprndu  7606  genpdisj  7607  addlocprlem  7619  nqprloc  7629  recexprlemss1l  7719  recexprlemss1u  7720  suplocexprlemss  7799  elrealeu  7913  ltleletr  8125  negf1o  8425  zletric  9387  zlelttric  9388  zltnle  9389  zmulcl  9396  zdcle  9419  zdclt  9420  zeo  9448  uz11  9641  indstr  9684  eqreznegel  9705  negm  9706  lbzbi  9707  fzdcel  10132  fzm1  10192  qletric  10348  qlelttric  10349  qltnle  10350  qdclt  10352  frecuzrdgtcl  10521  frecuzrdgfunlem  10528  qsqeqor  10759  rennim  11184  maxleast  11395  negfi  11410  fsum3cvg  11560  fproddccvg  11754  prodmodc  11760  ndvdssub  12112  bitsinv1lem  12143  algcvgblem  12242  algcvga  12244  isprm3  12311  oddprmdvds  12548  4sqlem2  12583  imasaddfnlemg  13016  subrngintm  13844  subrgintm  13875  lmodfopnelem1  13956  islssm  13989  lspsneq0  14058  islidlm  14111  epttop  14410  cnptoprest  14559  txcnp  14591  metequiv2  14816  cnlimcim  14991  bj-hbalt  15493  bj-intabssel1  15520  decidin  15527  sumdc2  15529  bj-charfunr  15540  bj-axemptylem  15622  bj-nnen2lp  15684  bj-nnord  15688  setindft  15695  bj-inf2vnlem2  15701  bj-inf2vnlem3  15702  bj-inf2vnlem4  15703  exmidsbthrlem  15753  triap  15760  tridceq  15787