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 ⊢ (𝜑 → (𝜓 → 𝜃))

This proof depends on syntax axioms:   → wi 4

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7

This theorem is used 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  454  con2d  633  con3d  640  expi  647  pm3.37  700  pm5.21ndd  717  pm2.37  817  pm2.81  823  dcim  853  condcOLD  866  con4biddc  869  pm2.54dc  903  pm4.79dc  915  pm2.85dc  917  pm3.12dc  971  dn1dc  973  3jao  1342  xoranor  1426  syl6an  1483  syl10  1484  hbald  1544  ax12  1565  hbimd  1626  nfal  1629  19.21ht  1634  19.30dc  1680  19.23t  1729  hbexd  1746  spimth  1788  spimed  1793  cbv2h  1801  cbv2w  1803  equvini  1811  sbiedh  1840  sbcof2  1863  aev  1865  sb3  1884  hbsb2  1889  sbequilem  1891  sbft  1901  sbi1v  1946  cbvexdh  1982  nf5-1  2084  mo23  2128  moexexdc  2171  euexex  2172  exists2  2184  dvelimdc  2413  rsp2  2600  rgen2a  2604  spcimgft  2901  spcimegft  2903  eueq3dc  3000  moeq3dc  3002  reu6  3015  ssddif  3465  reupick2  3519  ifnebibdc  3686  sssnm  3879  prneimg  3899  dfiun2g  4044  exmidsssnc  4340  exmidundifim  4344  opth1  4376  copsexg  4384  opelopabt  4404  issod  4464  sowlin  4465  suctr  4566  reusv3i  4605  ralxfrALT  4613  ssorduni  4634  onintonm  4664  regexmidlem1  4680  nlimsucg  4713  0elnn  4766  ssrelrn  4972  issref  5170  iotaval  5349  fun11iun  5660  brprcneu  5688  fvssunirng  5710  relfvssunirn  5711  fv3  5718  ndmfvg  5726  ssimaex  5764  fvopab3ig  5779  dff4im  5854  ffnfv  5866  fconstfvm  5933  f1mpt  5977  oprabid  6117  mpoeq123  6147  f1o2ndf1  6464  brtposg  6525  rntpos  6528  dftpos4  6534  smores2  6565  tfri3  6638  rdgss  6654  nntri3or  6766  nndifsnid  6780  nnawordex  6802  eroveu  6900  map0g  6969  fundmen  7094  nneneq  7158  fiintim  7238  snon0  7249  fnfi  7250  infnlbti  7366  exmidonfinlem  7545  exmidontri2or  7602  addclpi  7694  enq0tr  7801  genprndl  7888  genprndu  7889  genpdisj  7890  addlocprlem  7902  nqprloc  7912  recexprlemss1l  8002  recexprlemss1u  8003  suplocexprlemss  8082  elrealeu  8196  ltleletr  8407  negf1o  8709  zletric  9690  zlelttric  9691  zltnle  9692  zmulcl  9700  zdcle  9723  zdclt  9724  zeo  9753  uz11  9947  indstr  9995  eqreznegel  10016  negm  10017  lbzbi  10018  fzdcel  10446  fzm1  10509  qletric  10678  qlelttric  10679  qltnle  10680  qdclt  10682  frecuzrdgtcl  10851  frecuzrdgfunlem  10858  qsqeqor  11089  swrdccatin2d  11518  rennim  11770  maxleast  11981  negfi  11996  fsum3cvg  12147  fproddccvg  12341  prodmodc  12347  ndvdssub  12699  bitsinv1lem  12730  algcvgblem  12829  algcvga  12831  isprm3  12898  oddprmdvds  13135  4sqlem2  13170  ballotfilemfc0  13234  ballotfilemfcc  13235  imasaddfnlemg  13637  subrngintm  14522  subrgintm  14553  lmodfopnelem1  14663  islssm  14696  lspsneq0  14765  islidlm  14818  epttop  15193  cnptoprest  15342  txcnp  15374  metequiv2  15599  cnlimcim  15774  umgrclwwlkge2  16655  bj-hbalt  16803  bj-intabssel1  16830  decidin  16837  sumdc2  16839  bj-charfunr  16848  bj-axemptylem  16930  bj-nnen2lp  16992  bj-nnord  16996  setindft  17003  bj-inf2vnlem2  17009  bj-inf2vnlem3  17010  bj-inf2vnlem4  17011  exmidsbthrlem  17079  triap  17090  tridceq  17118