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  629  con3d  636  expi  643  pm3.37  695  pm5.21ndd  712  pm2.37  812  pm2.81  818  dcim  848  condcOLD  861  con4biddc  864  pm2.54dc  898  pm4.79dc  910  pm2.85dc  912  pm3.12dc  966  dn1dc  968  3jao  1337  xoranor  1421  syl6an  1478  syl10  1479  hbald  1539  ax12  1560  hbimd  1621  nfal  1624  19.21ht  1629  19.30dc  1675  19.23t  1725  hbexd  1742  spimth  1783  spimed  1788  cbv2h  1796  cbv2w  1798  equvini  1806  sbiedh  1835  sbcof2  1858  aev  1860  sb3  1879  hbsb2  1884  sbequilem  1886  sbft  1896  sbi1v  1940  cbvexdh  1975  nf5-1  2077  mo23  2121  moexexdc  2164  euexex  2165  exists2  2177  dvelimdc  2395  rsp2  2582  rgen2a  2586  spcimgft  2882  spcimegft  2884  eueq3dc  2980  moeq3dc  2982  reu6  2995  ssddif  3441  reupick2  3493  ifnebibdc  3651  sssnm  3837  prneimg  3857  dfiun2g  4002  exmidsssnc  4293  exmidundifim  4297  opth1  4328  copsexg  4336  opelopabt  4356  issod  4416  sowlin  4417  suctr  4518  reusv3i  4556  ralxfrALT  4564  ssorduni  4585  onintonm  4615  regexmidlem1  4631  nlimsucg  4664  0elnn  4717  ssrelrn  4922  issref  5119  iotaval  5298  fun11iun  5604  brprcneu  5632  fvssunirng  5654  relfvssunirn  5655  fv3  5662  ndmfvg  5670  ssimaex  5707  fvopab3ig  5720  dff4im  5793  ffnfv  5805  fconstfvm  5872  f1mpt  5912  oprabid  6050  mpoeq123  6080  f1o2ndf1  6393  brtposg  6420  rntpos  6423  dftpos4  6429  smores2  6460  tfri3  6533  rdgss  6549  nntri3or  6661  nndifsnid  6675  nnawordex  6697  eroveu  6795  map0g  6857  fundmen  6981  nneneq  7043  fiintim  7123  snon0  7134  fnfi  7135  infnlbti  7225  exmidonfinlem  7404  exmidontri2or  7461  addclpi  7547  enq0tr  7654  genprndl  7741  genprndu  7742  genpdisj  7743  addlocprlem  7755  nqprloc  7765  recexprlemss1l  7855  recexprlemss1u  7856  suplocexprlemss  7935  elrealeu  8049  ltleletr  8261  negf1o  8561  zletric  9523  zlelttric  9524  zltnle  9525  zmulcl  9533  zdcle  9556  zdclt  9557  zeo  9585  uz11  9779  indstr  9827  eqreznegel  9848  negm  9849  lbzbi  9850  fzdcel  10275  fzm1  10335  qletric  10502  qlelttric  10503  qltnle  10504  qdclt  10506  frecuzrdgtcl  10675  frecuzrdgfunlem  10682  qsqeqor  10913  swrdccatin2d  11326  rennim  11564  maxleast  11775  negfi  11790  fsum3cvg  11941  fproddccvg  12135  prodmodc  12141  ndvdssub  12493  bitsinv1lem  12524  algcvgblem  12623  algcvga  12625  isprm3  12692  oddprmdvds  12929  4sqlem2  12964  imasaddfnlemg  13399  subrngintm  14229  subrgintm  14260  lmodfopnelem1  14341  islssm  14374  lspsneq0  14443  islidlm  14496  epttop  14817  cnptoprest  14966  txcnp  14998  metequiv2  15223  cnlimcim  15398  umgrclwwlkge2  16256  bj-hbalt  16380  bj-intabssel1  16407  decidin  16414  sumdc2  16416  bj-charfunr  16426  bj-axemptylem  16508  bj-nnen2lp  16570  bj-nnord  16574  setindft  16581  bj-inf2vnlem2  16587  bj-inf2vnlem3  16588  bj-inf2vnlem4  16589  exmidsbthrlem  16647  triap  16654  tridceq  16681