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 4401  fundmen 4428  sbthbg 4458  sdomdomtr 4469  domsdomtr 4476  mapenlem2 4490  nneneq 4512  php 4513  php3 4515  php3OLD 4516  onomeneq 4519  pssnn 4534  unblem1 4540  fiint 4559  fiintOLD 4560  preleq 4603  inf3lem2 4614  inf3lem3 4615  inf3lem6 4618  zfregs 4647  r1tr 4654  r1ord2 4656  tz9.12lem3 4661  rankr1lem 4673  rankr1 4674  rankval3 4681  bndrank 4682  r1pwcl 4687  rankr1b 4699  cplem1 4720  karden 4726  hta 4728  aceq5lem4 4738  aceq5lem5 4739  aceq5 4740  aceq6b 4742  kmlem13 4777  weth 4787  zorn2lem4 4791  zorn2lem6 4793  unidom 4808  uniimadom 4810  carden 4831  carddom 4836  sucdom 4842  carduni 4858  cardmin 4860  alephordlem2 4873  alephordi 4874  cardinfima 4891  alephval2 4902  alephval3 4903  cfub 4908  cfsuc 4915  axextnd 4943  addclpi 5020  ltbtwnpq 5084  genpss 5107  genpnmax 5110  distrlem1pr 5127  ltaddpr 5140  reclem3pr 5158  reclem4pr 5159  suplem1pr 5161  suplem2pr 5162  ssgt0sr 5217  suppsrlem 5221  suppsr2 5223  suppsr3 5224  suprelem 5259  pre-axsup 5291  negeu 5355  receu 5701  nominpos 6043  lbinfm 6048  sup2 6051  infmrcl 6069  xrsupsslem 6076  xrinfmsslem 6077  supxrre 6083  supxrun 6085  supxrpnf 6088  supxrunb1 6089  supxrunb2 6090  zaddclt 6165  zmulclt 6180  zltp1let 6181  zeot 6199  uzindOLD 6208  uzwo4OLD 6210  qnegclt 6270  qbtwnre 6278  uz11t 6432  uzwo 6455  uzwoOLD 6456  fsequb 6523  nn0opthlem2 6665  sqr2irrlem3 6726  seq1bnd 6910  cau5i 6917  cvg1 6921  cvg3 6923  cvganz 6924  caubnd 6926  bccl2t 6971  fsumshftm 7032  clm3 7079  climshft 7104  climaddlem3 7116  climmullem8 7127  clim2serzt 7134  iserzext 7135  climsup 7155  caucvglem2 7158  caucvglem5 7161  caucvglem6 7162  expcnvlem6 7232  fsum0diaglem2 7257  elcncf 7265  ivthlem7 7287  efcltlem2 7305  efseq0ex 7311  infxpidmlem7 7558  infxpidmlem8 7559  infmap2lem1 7579  infmap2lem2 7580  tgclt 7624  basgen2t 7639  elcls 7704  cnpimaex 7765  cnpco 7769  opnuni 7868  caun0 7945  lmuni 7951  lmle 7960  metelcls 7965  metcnp4 7970  xplm 7975  iscms2lem4 7992  minveclem27 8571  psdmrn 8648  psref 8649  psasym 8651  pstr 8652  efifolem5 8726  efif1lem3 8732  chlim 9104  ocsh 9156  occllem6 9178  occllem7 9179  pjthlem12 9230  pjtheu 9235  shselt 9278  spansncol 9491  h1datom 9504  osumlem4 9581  cnopct 9837  cnfnct 9854  0cnop 9903  0cnfn 9904  idcnop 9905  riesz1t 9998  rnbra 10040  stm1add 10172  stm1add3 10174  cvnsymt 10217  mdbr2 10223  dmdbr2 10230  mdsl0 10237  mdsl1 10248  mdsl2 10249  cvmd 10251  atexcht 10308  atcvat4 10324  cdj1 10360  ghomf1olem 10396  ficli 10472  ficliOLD 10473  fiv 10482  fivOLD 10483  fiiu2 10488  fiiu2OLD 10489  bsi 10495  cnvhmpha 10525  hmeogrp 10538  homcard 10539  top2usne 10549  homindlem3 10551  fillsb 10560  filint 10562  efilcp 10572  efilcpOLD 10573  efilcp2 10581  efilcp2OLD 10582  cnfilca 10583  cnfilcaOLD 10584  rcfpfillem4 10591  rcfpfillem4OLD 10592  iintlem1 10632  cmpmorp 10712  ismonc 10742

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

Copyright terms: Public domain