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  4340  exmidundifim  4344  opth1  4376  copsexg  4384  opelopabt  4404  issod  4464  sowlin  4465  suctr  4566  reusv3i  4605  ralxfrALT  4613  ssorduni  4634  onintonm  4664  regexmidlem1  4680  nlimsucg  4713  0elnn  4766  ssrelrn  4972  issref  5170  iotaval  5349  fun11iun  5660  brprcneu  5688  fvssunirng  5710  relfvssunirn  5711  fv3  5718  ndmfvg  5726  ssimaex  5764  fvopab3ig  5779  dff4im  5854  ffnfv  5866  fconstfvm  5933  f1mpt  5977  oprabid  6117  mpoeq123  6147  f1o2ndf1  6464  brtposg  6525  rntpos  6528  dftpos4  6534  smores2  6565  tfri3  6638  rdgss  6654  nntri3or  6766  nndifsnid  6780  nnawordex  6802  eroveu  6900  map0g  6969  fundmen  7094  nneneq  7158  fiintim  7238  snon0  7249  fnfi  7250  infnlbti  7367  exmidonfinlem  7546  exmidontri2or  7603  addclpi  7695  enq0tr  7802  genprndl  7889  genprndu  7890  genpdisj  7891  addlocprlem  7903  nqprloc  7913  recexprlemss1l  8003  recexprlemss1u  8004  suplocexprlemss  8083  elrealeu  8197  ltleletr  8408  negf1o  8711  zletric  9693  zlelttric  9694  zltnle  9695  zmulcl  9703  zdcle  9726  zdclt  9727  zeo  9756  uz11  9955  indstr  10003  eqreznegel  10024  negm  10025  lbzbi  10026  fzdcel  10455  fzm1  10518  qletric  10687  qlelttric  10688  qltnle  10689  qdclt  10691  frecuzrdgtcl  10863  frecuzrdgfunlem  10870  qsqeqor  11101  swrdccatin2d  11531  rennim  11783  maxleast  11995  negfi  12010  fsum3cvg  12163  fproddccvg  12357  prodmodc  12363  ndvdssub  12715  bitsinv1lem  12746  algcvgblem  12845  algcvga  12847  isprm3  12914  oddprmdvds  13155  4sqlem2  13190  ballotfilemfc0  13283  ballotfilemfcc  13284  imasaddfnlemg  13686  subrngintm  14571  subrgintm  14602  lmodfopnelem1  14712  islssm  14745  lspsneq0  14814  islidlm  14867  epttop  15243  cnptoprest  15392  txcnp  15424  metequiv2  15649  cnlimcim  15824  ppiublem1  16213  umgrclwwlkge2  16765  bj-hbalt  16913  bj-intabssel1  16940  decidin  16947  sumdc2  16949  bj-charfunr  16958  bj-axemptylem  17040  bj-nnen2lp  17102  bj-nnord  17106  setindft  17113  bj-inf2vnlem2  17119  bj-inf2vnlem3  17120  bj-inf2vnlem4  17121  exmidsbthrlem  17189  triap  17200  tridceq  17228