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  625  con3d  632  expi  639  pm3.37  691  pm5.21ndd  707  pm2.37  807  pm2.81  813  dcim  843  condcOLD  856  con4biddc  859  pm2.54dc  893  pm4.79dc  905  pm2.85dc  907  pm3.12dc  961  dn1dc  963  3jao  1314  xoranor  1397  syl6an  1454  syl10  1455  hbald  1515  ax12  1536  hbimd  1597  nfal  1600  19.21ht  1605  19.30dc  1651  19.23t  1701  hbexd  1718  spimth  1759  spimed  1764  cbv2h  1772  cbv2w  1774  equvini  1782  sbiedh  1811  sbcof2  1834  aev  1836  sb3  1855  hbsb2  1860  sbequilem  1862  sbft  1872  sbi1v  1916  cbvexdh  1951  nf5-1  2053  mo23  2096  moexexdc  2139  euexex  2140  exists2  2152  dvelimdc  2370  rsp2  2557  rgen2a  2561  spcimgft  2850  spcimegft  2852  eueq3dc  2948  moeq3dc  2950  reu6  2963  ssddif  3408  reupick2  3460  ifnebibdc  3616  sssnm  3797  prneimg  3817  dfiun2g  3961  exmidsssnc  4251  exmidundifim  4255  opth1  4284  copsexg  4292  opelopabt  4312  issod  4370  sowlin  4371  suctr  4472  reusv3i  4510  ralxfrALT  4518  ssorduni  4539  onintonm  4569  regexmidlem1  4585  nlimsucg  4618  0elnn  4671  ssrelrn  4874  issref  5070  iotaval  5248  fun11iun  5550  brprcneu  5576  fvssunirng  5598  relfvssunirn  5599  fv3  5606  ndmfvg  5614  ssimaex  5647  fvopab3ig  5660  dff4im  5733  ffnfv  5745  fconstfvm  5809  f1mpt  5847  oprabid  5983  mpoeq123  6011  f1o2ndf1  6321  brtposg  6347  rntpos  6350  dftpos4  6356  smores2  6387  tfri3  6460  rdgss  6476  nntri3or  6586  nndifsnid  6600  nnawordex  6622  eroveu  6720  map0g  6782  fundmen  6905  nneneq  6961  fiintim  7035  snon0  7044  fnfi  7045  infnlbti  7135  exmidonfinlem  7308  exmidontri2or  7362  addclpi  7447  enq0tr  7554  genprndl  7641  genprndu  7642  genpdisj  7643  addlocprlem  7655  nqprloc  7665  recexprlemss1l  7755  recexprlemss1u  7756  suplocexprlemss  7835  elrealeu  7949  ltleletr  8161  negf1o  8461  zletric  9423  zlelttric  9424  zltnle  9425  zmulcl  9433  zdcle  9456  zdclt  9457  zeo  9485  uz11  9678  indstr  9721  eqreznegel  9742  negm  9743  lbzbi  9744  fzdcel  10169  fzm1  10229  qletric  10391  qlelttric  10392  qltnle  10393  qdclt  10395  frecuzrdgtcl  10564  frecuzrdgfunlem  10571  qsqeqor  10802  rennim  11357  maxleast  11568  negfi  11583  fsum3cvg  11733  fproddccvg  11927  prodmodc  11933  ndvdssub  12285  bitsinv1lem  12316  algcvgblem  12415  algcvga  12417  isprm3  12484  oddprmdvds  12721  4sqlem2  12756  imasaddfnlemg  13190  subrngintm  14018  subrgintm  14049  lmodfopnelem1  14130  islssm  14163  lspsneq0  14232  islidlm  14285  epttop  14606  cnptoprest  14755  txcnp  14787  metequiv2  15012  cnlimcim  15187  bj-hbalt  15773  bj-intabssel1  15800  decidin  15807  sumdc2  15809  bj-charfunr  15820  bj-axemptylem  15902  bj-nnen2lp  15964  bj-nnord  15968  setindft  15975  bj-inf2vnlem2  15981  bj-inf2vnlem3  15982  bj-inf2vnlem4  15983  exmidsbthrlem  16035  triap  16042  tridceq  16069