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  1502  ax12  1523  hbimd  1584  nfal  1587  19.21ht  1592  19.30dc  1638  19.23t  1688  hbexd  1705  spimth  1746  spimed  1751  cbv2h  1759  cbv2w  1761  equvini  1769  sbiedh  1798  sbcof2  1821  aev  1823  sb3  1842  hbsb2  1847  sbequilem  1849  sbft  1859  sbi1v  1903  cbvexdh  1938  nf5-1  2036  mo23  2079  moexexdc  2122  euexex  2123  exists2  2135  dvelimdc  2353  rsp2  2540  rgen2a  2544  spcimgft  2828  spcimegft  2830  eueq3dc  2926  moeq3dc  2928  reu6  2941  ssddif  3384  reupick2  3436  sssnm  3769  prneimg  3789  dfiun2g  3933  exmidsssnc  4221  exmidundifim  4225  opth1  4254  copsexg  4262  opelopabt  4280  issod  4337  sowlin  4338  suctr  4439  reusv3i  4477  ralxfrALT  4485  ssorduni  4504  onintonm  4534  regexmidlem1  4550  nlimsucg  4583  0elnn  4636  issref  5029  iotaval  5207  fun11iun  5501  brprcneu  5527  fvssunirng  5549  relfvssunirn  5550  fv3  5557  ndmfvg  5565  ssimaex  5597  fvopab3ig  5610  dff4im  5682  ffnfv  5694  fconstfvm  5754  f1mpt  5792  oprabid  5927  mpoeq123  5954  f1o2ndf1  6252  brtposg  6278  rntpos  6281  dftpos4  6287  smores2  6318  tfri3  6391  rdgss  6407  nntri3or  6517  nndifsnid  6531  nnawordex  6553  eroveu  6651  map0g  6713  fundmen  6831  nneneq  6884  fiintim  6956  snon0  6964  fnfi  6965  infnlbti  7054  exmidonfinlem  7221  exmidontri2or  7271  addclpi  7355  enq0tr  7462  genprndl  7549  genprndu  7550  genpdisj  7551  addlocprlem  7563  nqprloc  7573  recexprlemss1l  7663  recexprlemss1u  7664  suplocexprlemss  7743  elrealeu  7857  ltleletr  8068  negf1o  8368  zletric  9326  zlelttric  9327  zltnle  9328  zmulcl  9335  zdcle  9358  zdclt  9359  zeo  9387  uz11  9579  indstr  9622  eqreznegel  9643  negm  9644  lbzbi  9645  fzdcel  10069  fzm1  10129  qletric  10273  qlelttric  10274  qltnle  10275  frecuzrdgtcl  10442  frecuzrdgfunlem  10449  qsqeqor  10661  rennim  11042  maxleast  11253  negfi  11267  fsum3cvg  11417  fproddccvg  11611  prodmodc  11617  ndvdssub  11966  algcvgblem  12080  algcvga  12082  isprm3  12149  oddprmdvds  12385  4sqlem2  12420  imasaddfnlemg  12788  subrngintm  13556  subrgintm  13587  lmodfopnelem1  13637  islssm  13670  lspsneq0  13739  islidlm  13792  epttop  14042  cnptoprest  14191  txcnp  14223  metequiv2  14448  cnlimcim  14592  bj-hbalt  14968  bj-intabssel1  14995  decidin  15002  sumdc2  15004  bj-charfunr  15015  bj-axemptylem  15097  bj-nnen2lp  15159  bj-nnord  15163  setindft  15170  bj-inf2vnlem2  15176  bj-inf2vnlem3  15177  bj-inf2vnlem4  15178  exmidsbthrlem  15224  triap  15231  tridceq  15258