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  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  3877  prneimg  3897  dfiun2g  4042  exmidsssnc  4338  exmidundifim  4342  opth1  4374  copsexg  4382  opelopabt  4402  issod  4462  sowlin  4463  suctr  4564  reusv3i  4603  ralxfrALT  4611  ssorduni  4632  onintonm  4662  regexmidlem1  4678  nlimsucg  4711  0elnn  4764  ssrelrn  4970  issref  5168  iotaval  5347  fun11iun  5658  brprcneu  5686  fvssunirng  5708  relfvssunirn  5709  fv3  5716  ndmfvg  5724  ssimaex  5761  fvopab3ig  5776  dff4im  5848  ffnfv  5860  fconstfvm  5927  f1mpt  5971  oprabid  6111  mpoeq123  6141  f1o2ndf1  6458  brtposg  6519  rntpos  6522  dftpos4  6528  smores2  6559  tfri3  6632  rdgss  6648  nntri3or  6760  nndifsnid  6774  nnawordex  6796  eroveu  6894  map0g  6963  fundmen  7088  nneneq  7152  fiintim  7232  snon0  7243  fnfi  7244  infnlbti  7360  exmidonfinlem  7539  exmidontri2or  7596  addclpi  7688  enq0tr  7795  genprndl  7882  genprndu  7883  genpdisj  7884  addlocprlem  7896  nqprloc  7906  recexprlemss1l  7996  recexprlemss1u  7997  suplocexprlemss  8076  elrealeu  8190  ltleletr  8401  negf1o  8703  zletric  9671  zlelttric  9672  zltnle  9673  zmulcl  9681  zdcle  9704  zdclt  9705  zeo  9734  uz11  9928  indstr  9976  eqreznegel  9997  negm  9998  lbzbi  9999  fzdcel  10427  fzm1  10490  qletric  10659  qlelttric  10660  qltnle  10661  qdclt  10663  frecuzrdgtcl  10832  frecuzrdgfunlem  10839  qsqeqor  11070  swrdccatin2d  11499  rennim  11751  maxleast  11962  negfi  11977  fsum3cvg  12128  fproddccvg  12322  prodmodc  12328  ndvdssub  12680  bitsinv1lem  12711  algcvgblem  12810  algcvga  12812  isprm3  12879  oddprmdvds  13116  4sqlem2  13151  ballotfilemfc0  13215  ballotfilemfcc  13216  imasaddfnlemg  13618  subrngintm  14503  subrgintm  14534  lmodfopnelem1  14644  islssm  14677  lspsneq0  14746  islidlm  14799  epttop  15174  cnptoprest  15323  txcnp  15355  metequiv2  15580  cnlimcim  15755  umgrclwwlkge2  16626  bj-hbalt  16774  bj-intabssel1  16801  decidin  16808  sumdc2  16810  bj-charfunr  16819  bj-axemptylem  16901  bj-nnen2lp  16963  bj-nnord  16967  setindft  16974  bj-inf2vnlem2  16980  bj-inf2vnlem3  16981  bj-inf2vnlem4  16982  exmidsbthrlem  17041  triap  17052  tridceq  17080