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 571  pm2.81 577  pm4.71 635  pm5.21nd 680  pclem6 741  oplem1 772  3jao 886  meredith 924  ax4 972  hbald 1113  hbexd 1114  19.21t 1115  equs4 1150  a4imt 1158  cbv1 1162  cbv2 1163  sbied 1195  sb3 1222  dfsb2 1225  hbsb2 1227  sbn 1231  sbi1 1232  hbsb4 1248  sb9i 1263  sbal1 1346  ax11eq 1363  ax11el 1364  ax11indn 1366  ax11indi 1367  a12stdy2 1373  mo 1393  moexex 1438  2mo 1447  2eu1 1449  ra42 1696  rgen2a 1699  mo2icl 1923  reu3 1931  csbie2t 2033  uniiunlem 2132  pwpw0 2469  sssn 2473  pwsnALT 2501  ss2iun 2577  iineq2 2579  dfiun2g 2586  trel 2687  axsep 2702  opth 2787  ralxfr 2899  frirr 2924  wefrc 2943  tz7.7 2973  onfr 2986  ordsson 2991  ssorduni 2993  ordunidif 3005  oneqmini 3017  suceloni 3062  ordunisuc2 3115  tfinds 3161  ssnlim 3167  brrelex 3207  weinxp 3233  ssrel 3247  fv3 3733  ndmfv 3745  ssimaex 3768  chfnrn 3802  dff2 3817  dff3 3818  ffnfv 3828  fconstfv 3849  elunirnALT 3869  isomin 3899  isofrlem 3901  f1oweALT 3906  iunon 3909  iinon 3910  tfrlem1 3911  tfr3 3926  rdglim2 3949  tz7.48lem 3955  tz7.49 3959  abianfp 3962  oawordex 4191  oa00 4193  oaass 4195  oarec 4196  om00 4206  odi 4210  omass 4211  oeordi 4214  oelim2 4222  nneob 4255  omsmolem 4256  omsmo 4257  ereldm 4285  erdisj 4286  eceqopreq 4313  en3d 4400  fundmen 4427  sbthbg 4456  sdomdomtr 4467  domsdomtr 4474  mapenlem2 4488  nneneq 4510  php 4511  php3 4513  onomeneq 4516  pssnn 4531  unblem1 4535  fiint 4552  preleq 4595  inf3lem2 4606  inf3lem3 4607  inf3lem6 4610  zfregs 4639  r1tr 4646  r1ord2 4648  tz9.12lem3 4653  rankr1lem 4665  rankr1 4666  rankval3 4673  bndrank 4674  r1pwcl 4679  rankr1b 4691  cplem1 4712  karden 4718  hta 4720  aceq5lem4 4730  aceq5lem5 4731  aceq5 4732  aceq6b 4734  kmlem13 4769  weth 4779  zorn2lem4 4783  zorn2lem6 4785  unidom 4800  uniimadom 4802  carden 4823  carddom 4828  sucdom 4834  carduni 4850  cardmin 4852  alephordlem2 4865  alephordi 4866  cardinfima 4883  alephval2 4894  alephval3 4895  cfub 4900  cfsuc 4907  axextnd 4935  addclpi 5012  ltbtwnpq 5076  genpss 5099  genpnmax 5102  distrlem1pr 5119  ltaddpr 5132  reclem3pr 5150  reclem4pr 5151  suplem1pr 5153  suplem2pr 5154  ssgt0sr 5209  suppsrlem 5213  suppsr2 5215  suppsr3 5216  suprelem 5251  pre-axsup 5283  negeu 5347  receu 5689  nominpos 6031  lbinfm 6036  sup2 6039  infmrcl 6057  xrsupsslem 6064  xrinfmsslem 6065  supxrre 6071  supxrun 6073  supxrpnf 6076  supxrunb1 6077  supxrunb2 6078  zaddclt 6153  zmulclt 6168  zltp1let 6169  zeot 6187  uzindOLD 6196  uzwo4OLD 6198  qnegclt 6256  qbtwnre 6264  uz11t 6418  uzwo 6441  uzwoOLD 6442  fsequb 6509  nn0opthlem2 6651  sqr2irrlem3 6712  seq1bnd 6895  cau5i 6902  cvg1 6906  cvg3 6908  cvganz 6909  caubnd 6911  bccl2t 6956  fsumshftm 7017  clm3 7064  climshft 7089  climaddlem3 7101  climmullem8 7112  clim2serzt 7119  iserzext 7120  climsup 7140  caucvglem2 7143  caucvglem5 7146  caucvglem6 7147  expcnvlem6 7217  fsum0diaglem2 7242  elcncf 7250  ivthlem7 7272  efcltlem2 7290  efseq0ex 7296  infxpidmlem7 7543  infxpidmlem8 7544  infmap2lem1 7564  infmap2lem2 7565  tgclt 7609  basgen2t 7624  elcls 7689  cnpimaex 7750  cnpco 7754  opnuni 7853  caun0 7930  lmuni 7936  lmle 7945  metelcls 7950  metcnp4 7955  xplm 7960  iscms2lem4 7977  minveclem27 8556  psdmrn 8633  psref 8634  psasym 8636  pstr 8637  efifolem5 8711  efif1lem3 8717  chlim 9089  ocsh 9141  occllem6 9163  occllem7 9164  pjthlem12 9215  pjtheu 9220  shselt 9263  spansncol 9476  h1datom 9489  osumlem4 9566  cnopct 9822  cnfnct 9839  0cnop 9888  0cnfn 9889  idcnop 9890  riesz1t 9983  rnbra 10025  stm1add 10157  stm1add3 10159  cvnsymt 10202  mdbr2 10208  dmdbr2 10215  mdsl0 10222  mdsl1 10233  mdsl2 10234  cvmd 10236  atexcht 10293  atcvat4 10309  cdj1 10345  ghomf1olem 10381  ficli 10451  fiv 10459  fiiu2 10462  bsi 10467  cnvhmpha 10497  hmeogrp 10510  homcard 10511  fillsb 10520  filint 10522  efilcp 10530  efilcp2 10536  cnfilca 10537  rcfpfillem4 10541  iintlem1 10575  cmpmorp 10655  ismonc 10683

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

Copyright terms: Public domain