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  6530  rntpos  6533  dftpos4  6539  smores2  6570  tfri3  6643  rdgss  6659  nntri3or  6771  nndifsnid  6785  nnawordex  6807  eroveu  6905  map0g  6974  fundmen  7100  nneneq  7164  fiintim  7244  snon0  7255  fnfi  7256  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  9698  zlelttric  9699  zltnle  9700  zmulcl  9708  zdcle  9731  zdclt  9732  zeo  9762  uz11  9961  indstr  10009  eqreznegel  10030  negm  10031  lbzbi  10032  fzdcel  10461  fzm1  10524  qletric  10693  qlelttric  10694  qltnle  10695  qdclt  10697  frecuzrdgtcl  10870  frecuzrdgfunlem  10877  qsqeqor  11108  swrdccatin2d  11538  rennim  11790  maxleast  12002  negfi  12017  fsum3cvg  12170  fproddccvg  12364  prodmodc  12370  ndvdssub  12722  bitsinv1lem  12753  algcvgblem  12852  algcvga  12854  isprm3  12921  oddprmdvds  13162  4sqlem2  13197  ballotfilemfc0  13290  ballotfilemfcc  13291  imasaddfnlemg  13694  subrngintm  14629  subrgintm  14660  lmodfopnelem1  14770  islssm  14803  lspsneq0  14872  islidlm  14925  mvrf1fi  15231  epttop  15349  cnptoprest  15498  txcnp  15530  metequiv2  15755  cnlimcim  15930  ppiublem1  16324  umgrclwwlkge2  16881  bj-hbalt  17029  bj-intabssel1  17056  decidin  17063  sumdc2  17065  bj-charfunr  17074  bj-axemptylem  17156  bj-nnen2lp  17218  bj-nnord  17222  setindft  17229  bj-inf2vnlem2  17235  bj-inf2vnlem3  17236  bj-inf2vnlem4  17237  exmidsbthrlem  17306  triap  17317  tridceq  17346