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 570  pm2.81 576  pm4.71 634  pm5.21nd 679  pclem6 740  oplem1 771  3jao 884  meredith 922  ax4 970  hbald 1111  hbexd 1112  19.21t 1113  equs4 1148  a4imt 1156  cbv1 1160  cbv2 1161  sbied 1193  sb3 1220  dfsb2 1223  hbsb2 1225  sbn 1229  sbi1 1230  hbsb4 1246  sb9i 1261  sbal1 1344  ax11eq 1361  ax11el 1362  ax11indn 1364  ax11indi 1365  a12stdy2 1371  mo 1391  moexex 1436  2mo 1445  2eu1 1447  ra42 1693  rgen2a 1696  mo2icl 1919  reu3 1927  csbie2t 2029  uniiunlem 2128  pwpw0 2465  sssn 2469  ss2iun 2572  iineq2 2574  dfiun2g 2581  trel 2682  axsep 2697  opth 2782  ralxfr 2894  frirr 2919  wefrc 2938  tz7.7 2968  onfr 2981  ordsson 2986  ssorduni 2988  ordunidif 3000  oneqmini 3012  suceloni 3057  ordunisuc2 3110  tfinds 3156  ssnlim 3162  brrelex 3202  weinxp 3228  ssrel 3242  fv3 3724  ndmfv 3736  ssimaex 3759  chfnrn 3793  dff2 3808  dff3 3809  ffnfv 3819  fconstfv 3840  elunirnALT 3860  isomin 3890  isofrlem 3892  f1oweALT 3897  iunon 3900  iinon 3901  tfrlem1 3902  tfr3 3917  rdglim2 3940  tz7.48lem 3946  tz7.49 3950  abianfp 3953  oawordex 4181  oa00 4183  oaass 4185  oarec 4186  om00 4196  odi 4200  omass 4201  oeordi 4204  oelim2 4212  nneob 4245  omsmolem 4246  omsmo 4247  ereldm 4275  erdisj 4276  eceqopreq 4303  en3d 4388  fundmen 4415  sbthbg 4444  sdomdomtr 4455  domsdomtr 4462  mapenlem2 4476  nneneq 4498  php 4499  php3 4501  onomeneq 4504  pssnn 4519  unblem1 4523  fiint 4540  preleq 4583  inf3lem2 4594  inf3lem3 4595  inf3lem6 4598  zfregs 4627  r1tr 4634  r1ord2 4636  tz9.12lem3 4641  rankr1lem 4653  rankr1 4654  rankval3 4661  bndrank 4662  r1pwcl 4667  rankr1b 4679  cplem1 4700  karden 4706  hta 4708  aceq5lem4 4718  aceq5lem5 4719  aceq5 4720  aceq6b 4722  kmlem13 4757  weth 4767  zorn2lem4 4771  zorn2lem6 4773  unidom 4788  uniimadom 4790  carden 4811  carddom 4816  sucdom 4822  carduni 4838  cardmin 4840  alephordlem2 4853  alephordi 4854  cardinfima 4871  alephval2 4882  alephval3 4883  cfub 4888  cfsuc 4895  axextnd 4923  addclpi 5000  ltbtwnpq 5064  genpss 5087  genpnmax 5090  distrlem1pr 5107  ltaddpr 5120  reclem3pr 5138  reclem4pr 5139  suplem1pr 5141  suplem2pr 5142  ssgt0sr 5197  suppsrlem 5201  suppsr2 5203  suppsr3 5204  suprelem 5239  pre-axsup 5271  negeu 5335  receu 5678  nominpos 5998  lbinfm 6003  sup2 6006  infmrcl 6024  xrsupsslem 6031  xrinfmsslem 6032  supxrre 6038  supxrun 6040  supxrpnf 6043  supxrunb1 6044  supxrunb2 6045  zaddclt 6120  zmulclt 6135  zltp1let 6136  zeot 6154  uzindOLD 6164  uzwo4OLD 6166  qnegclt 6216  qbtwnre 6224  uz11t 6372  uzwo 6395  uzwoOLD 6396  fsequb 6463  nn0opthlem2 6603  sqr2irrlem3 6664  seq1bnd 6855  cau5i 6862  cvg1 6866  cvg3 6868  cvganz 6869  caubnd 6871  bccl2t 6917  fsumshftm 6978  clm3 7025  climshft 7049  climaddlem3 7060  climmullem8 7071  clim2serzt 7078  iserzext 7079  climsup 7099  caucvglem2 7102  caucvglem5 7105  caucvglem6 7106  expcnvlem6 7175  fsum0diaglem2 7200  elcncf 7208  ivthlem7 7230  ivthlem7OLD 7239  efcltlem2 7255  efseq0ex 7261  infxpidmlem7 7509  infxpidmlem8 7510  infmap2lem1 7529  infmap2lem2 7530  tgclt 7574  basgen2t 7589  elcls 7654  cnpimaex 7715  cnpco 7719  opnuni 7820  caun0 7896  lmuni 7902  lmle 7911  metelcls 7916  metcnp4 7920  xplm 7925  iscms2lem4 7942  minveclem27 8515  psdmrn 8591  psref 8592  psasym 8593  pstr 8594  efifolem5 8660  efif1lem3 8666  chlim 9043  ocsh 9095  occllem6 9117  occllem7 9118  pjthlem12 9168  pjtheu 9173  shselt 9216  spansncol 9430  h1datom 9444  osumlem4 9521  cnopct 9776  cnfnct 9793  0cnop 9842  0cnfn 9843  idcnop 9844  riesz1t 9936  rnbra 9978  stm1add 10110  stm1add3 10112  cvnsymt 10155  mdbr2 10161  dmdbr2 10168  mdsl0 10174  mdsl1 10185  mdsl2 10186  cvmd 10188  atexcht 10245  atcvat4 10261  cdj1 10294  ghomf1olem 10330  ficli 10404  fiv 10410  fiiu2 10413  bsi 10418  cnvhmpha 10448  hmeogrp 10461  homcard 10462  fillsb 10471  filint 10473  efilcp 10481  efilcp2 10486  cnfilca 10487  iintlem1 10512  cmpmorp 10592  ismonc 10620

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

Copyright terms: Public domain