Theorem syl6 22

Description: A syllogism rule of inference. The second premise is used to replace the consequent of the first premise.

Hypotheses

Ref	Expression
syl6.1	|- (ph -> (ps -> ch))
syl6.2	|- (ch -> th)

Assertion

Ref	Expression
syl6	|- (ph -> (ps -> th))

Proof of Theorem syl6

Step	Hyp	Ref	Expression
1		syl6.1	. 2 |- (ph -> (ps -> ch))
2		syl6.2	. . 3 |- (ch -> th)
3	2	imim2i 17	. 2 |- ((ps -> ch) -> (ps -> th))
4	1, 3	syl 10	1 |- (ph -> (ps -> th))

Syntax hints:   -> wi 3

This theorem is referenced by:  syl7 23  syl8 24  com34 36  a1dd 42  syldd 50  syl6com 53  looinv 83  pm2.61-ocatOLD 125  syl6ib 212  syl6ibr 213  syl6bi 214  syl6bir 215  jao 340  pm2.37 569  pm2.81 575  pm4.71 633  pm5.21nd 678  pclem6 739  oplem1 770  3jao 883  meredith 921  ax4 969  hbald 1109  hbexd 1110  19.21t 1111  equs4 1146  a4imt 1154  cbv1 1158  cbv2 1159  sbied 1191  sb3 1217  dfsb2 1220  hbsb2 1222  sbn 1226  sbi1 1227  hbsb4 1243  sb9i 1258  sbal1 1341  ax11eq 1356  ax11el 1357  ax11indn 1359  ax11indi 1360  a12stdy2 1366  mo 1386  moexex 1431  2mo 1440  2eu1 1442  ra42 1688  rgen2a 1691  mo2icl 1914  reu3 1921  csbie2t 2023  uniiunlem 2122  pwpw0 2460  sssn 2464  ss2iun 2567  iineq2 2569  dfiun2g 2576  trel 2677  axsep 2692  opth 2777  ralxfr 2889  frirr 2914  wefrc 2933  tz7.7 2963  onfr 2976  ordsson 2981  ssorduni 2983  ordunidif 2995  oneqmini 3007  suceloni 3052  ordunisuc2 3105  tfinds 3151  ssnlim 3157  brrelex 3197  weinxp 3223  ssrel 3237  fv3 3718  ndmfv 3730  ssimaex 3753  chfnrn 3787  dff2 3802  dff3 3803  ffnfv 3813  fconstfv 3834  elunirnALT 3854  isomin 3884  isofrlem 3886  f1oweALT 3891  iunon 3894  iinon 3895  tfrlem1 3896  tfr3 3911  rdglim2 3934  tz7.48lem 3940  tz7.49 3944  abianfp 3947  oawordex 4175  oa00 4177  oaass 4179  oarec 4180  om00 4190  odi 4194  omass 4195  oeordi 4198  oelim2 4206  nneob 4239  omsmolem 4240  omsmo 4241  ereldm 4269  erdisj 4270  eceqopreq 4297  en3d 4382  fundmen 4409  sbthbg 4438  sdomdomtr 4449  domsdomtr 4456  mapenlem2 4470  nneneq 4492  php 4493  php3 4495  onomeneq 4498  pssnn 4513  unblem1 4517  fiint 4534  preleq 4575  inf3lem2 4586  inf3lem3 4587  inf3lem6 4590  zfregs 4619  r1tr 4626  r1ord2 4628  tz9.12lem3 4633  rankr1lem 4645  rankr1 4646  rankval3 4653  bndrank 4654  r1pwcl 4659  rankr1b 4671  cplem1 4692  karden 4698  hta 4700  aceq5lem4 4710  aceq5lem5 4711  aceq5 4712  aceq6b 4714  kmlem13 4749  weth 4759  zorn2lem4 4763  zorn2lem6 4765  unidom 4780  uniimadom 4782  carden 4803  carddom 4808  sucdom 4814  carduni 4830  cardmin 4832  alephordlem2 4845  alephordi 4846  cardinfima 4863  alephval2 4874  alephval3 4875  cfub 4880  cfsuc 4887  axextnd 4915  addclpi 4992  ltbtwnpq 5056  genpss 5079  genpnmax 5082  distrlem1pr 5099  ltaddpr 5112  reclem3pr 5130  reclem4pr 5131  suplem1pr 5133  suplem2pr 5134  ssgt0sr 5189  suppsrlem 5193  suppsr2 5195  suppsr3 5196  suprelem 5231  pre-axsup 5263  negeu 5327  receu 5670  nominpos 5990  lbinfm 5995  sup2 5998  infmrcl 6016  xrsupsslem 6023  xrinfmsslem 6024  supxrre 6030  supxrun 6032  supxrpnf 6035  supxrunb1 6036  supxrunb2 6037  zaddclt 6112  zmulclt 6127  zltp1let 6128  zeot 6146  uzindOLD 6156  uzwo4OLD 6158  qnegclt 6208  qbtwnre 6216  uz11t 6364  uzwo 6387  uzwoOLD 6388  fsequb 6455  nn0opthlem2 6595  sqr2irrlem3 6656  seq1bnd 6847  cau5i 6854  cvg1 6858  cvg3 6860  cvganz 6861  caubnd 6863  bccl2t 6909  fsumshftm 6970  clm3 7017  climshft 7041  climaddlem3 7052  climmullem8 7063  clim2serzt 7070  iserzext 7071  climsup 7091  caucvglem2 7094  caucvglem5 7097  caucvglem6 7098  expcnvlem6 7167  fsum0diaglem2 7192  elcncf 7200  ivthlem7 7222  ivthlem7OLD 7231  efcltlem2 7247  efseq0ex 7253  infxpidmlem7 7501  infxpidmlem8 7502  infmap2lem1 7521  infmap2lem2 7522  tgclt 7566  basgen2t 7581  elcls 7646  cnpimaex 7704  cnpco 7708  opnuni 7808  caun0 7880  lmuni 7886  lmle 7895  metelcls 7900  metcnp4 7904  xplm 7909  iscms2lem4 7926  minveclem27 8502  psdmrn 8574  psref 8575  psasym 8576  efifolem5 8641  efif1lem3 8647  chlim 9025  ocsh 9072  occllem6 9094  occllem7 9095  pjthlem12 9145  pjtheu 9150  shselt 9193  spansncol 9407  h1datom 9421  osumlem4 9498  cnopct 9753  cnfnct 9770  0cnop 9819  0cnfn 9820  idcnop 9821  riesz1t 9913  rnbra 9953  stm1add 10082  stm1add3 10084  cvnsymt 10127  mdbr2 10133  dmdbr2 10140  mdsl0 10145  mdsl1 10156  mdsl2 10157  cvmd 10159  atexcht 10216  atcvat4 10232  cdj1 10265  ghomf1olem 10301  ficli 10368  fiv 10374  fiiu2 10377  bsi 10382  cnvhmpha 10412  hmeogrp 10425  homcard 10426  fillsb 10435  filint 10437  efilcp 10445  efilcp2 10450  cnfilca 10451  iintlem1 10476  cmpmorp 10556  ismonc 10584

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-mp 7

Copyright terms: Public domain