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  4342  exmidundifim  4346  opth1  4378  copsexg  4386  opelopabt  4406  issod  4466  sowlin  4467  suctr  4568  reusv3i  4607  ralxfrALT  4615  ssorduni  4636  onintonm  4666  regexmidlem1  4682  nlimsucg  4715  0elnn  4768  ssrelrn  4974  issref  5173  iotaval  5352  fun11iun  5663  brprcneu  5691  fvssunirng  5713  relfvssunirn  5714  fv3  5721  ndmfvg  5729  ssimaex  5767  fvopab3ig  5782  dff4im  5857  ffnfv  5869  fconstfvm  5936  f1mpt  5980  oprabid  6120  mpoeq123  6150  f1o2ndf1  6468  brtposg  6529  rntpos  6532  dftpos4  6538  smores2  6569  tfri3  6642  rdgss  6658  nntri3or  6770  nndifsnid  6784  nnawordex  6806  eroveu  6904  map0g  6973  fundmen  7099  nneneq  7163  fiintim  7243  snon0  7254  fnfi  7255  infnlbti  7373  exmidonfinlem  7552  exmidontri2or  7609  addclpi  7701  enq0tr  7808  genprndl  7895  genprndu  7896  genpdisj  7897  addlocprlem  7909  nqprloc  7919  recexprlemss1l  8009  recexprlemss1u  8010  suplocexprlemss  8089  elrealeu  8203  ltleletr  8414  negf1o  8717  zletric  9700  zlelttric  9701  zltnle  9702  zmulcl  9710  zdcle  9733  zdclt  9734  zeo  9763  uz11  9962  indstr  10010  eqreznegel  10031  negm  10032  lbzbi  10033  fzdcel  10462  fzm1  10525  qletric  10694  qlelttric  10695  qltnle  10696  qdclt  10698  frecuzrdgtcl  10871  frecuzrdgfunlem  10878  qsqeqor  11109  swrdccatin2d  11539  rennim  11791  maxleast  12003  negfi  12018  fsum3cvg  12171  fproddccvg  12365  prodmodc  12371  ndvdssub  12723  bitsinv1lem  12754  algcvgblem  12853  algcvga  12855  isprm3  12922  oddprmdvds  13163  4sqlem2  13198  ballotfilemfc0  13291  ballotfilemfcc  13292  imasaddfnlemg  13695  subrngintm  14630  subrgintm  14661  lmodfopnelem1  14771  islssm  14804  lspsneq0  14873  islidlm  14926  mvrf1fi  15215  epttop  15328  cnptoprest  15477  txcnp  15509  metequiv2  15734  cnlimcim  15909  ppiublem1  16303  umgrclwwlkge2  16860  bj-hbalt  17008  bj-intabssel1  17035  decidin  17042  sumdc2  17044  bj-charfunr  17053  bj-axemptylem  17135  bj-nnen2lp  17197  bj-nnord  17201  setindft  17208  bj-inf2vnlem2  17214  bj-inf2vnlem3  17215  bj-inf2vnlem4  17216  exmidsbthrlem  17285  triap  17296  tridceq  17325