Theorem sylbi 199

Description: A mixed syllogism inference from a biconditional and an implication. Useful for substituting an antecedent with a definition.

Hypotheses

Ref	Expression
sylbi.1	|- (ph <-> ps)
sylbi.2	|- (ps -> ch)

Assertion

Ref	Expression
sylbi	|- (ph -> ch)

Proof of Theorem sylbi

Step	Hyp	Ref	Expression
1		sylbi.1	. . 3 |- (ph <-> ps)
2	1	biimp 151	. 2 |- (ph -> ps)
3		sylbi.2	. 2 |- (ps -> ch)
4	2, 3	syl 10	1 |- (ph -> ch)

Syntax hints:   -> wi 3   <-> wb 146

This theorem is referenced by:  3imtr4 219  pm3.26 319  pm3.27 323  ancoms 438  an1s 488  an1rs 491  an4s 510  pm2.85 581  ordi 598  pm5.18 662  ccase 757  3simpb 788  3simpc 789  3imp 829  3com13 840  syl3anb 871  a6e 992  19.33b 1094  exintrbi 1120  equvini 1170  sb6x 1190  equs5e 1200  hbsb4t 1251  a12stdy2 1375  a12lem2 1379  euex 1396  eumo0 1397  mooran2 1428  mopick 1435  euor2 1440  2euex 1444  2mo 1450  2eu3 1454  exists2 1461  eqcoms 1481  necon3ai 1609  necon1ai 1611  rexex 1696  ra4 1697  r19.20 1705  r19.22 1734  r19.23ai 1745  r19.36av 1763  r19.37av 1764  r19.44av 1769  r19.45av 1770  elisset 1820  gencl 1831  vtoclgf 1849  cla4gf 1863  rcla4 1874  mo2icl 1926  moi2 1927  moi 1928  reu6 1935  2reuswap 1940  ra4sbc 2001  ra5 2004  sstr2 2075  pssn2lp 2151  ssnpss 2153  unineq 2259  reuun2 2282  disjssun 2331  pssnel 2336  difin0ss 2337  r19.2z 2352  r19.3rzv 2353  ralidm 2362  ifbi 2376  prprc1 2457  pwpw0 2474  sspr 2480  snsssn 2483  preqr2 2487  preq12b 2488  opthpr 2490  opprc1 2503  pwsnALT 2506  intmin4 2564  iunconst 2577  ssiun 2597  iununi 2622  trss 2695  axrep5 2704  zfrep4 2707  ssex 2725  intex 2735  intnex 2736  intabs 2739  snex 2757  rext 2761  unipw 2763  sspwuni 2765  moabex 2773  nnullss 2775  exss 2776  axpr 2785  opth 2794  copsexg 2799  opprc3 2804  ssopab2 2829  pwssun 2834  solin 2864  euuni 2888  reucl 2892  reuunisn 2902  reuxfr 2911  reuunixfr 2913  elpwunsn 2919  frc 2927  frirr 2931  fr2nr 2932  fr3nr 2933  onfr 2993  nlim0 3034  limord 3035  limuni 3036  elsuci 3042  sucprc 3051  onmindif2 3068  suceloni 3069  ordpwsuc 3073  onsucmin 3079  ordsucelsuc 3080  ordssun 3086  ordequn 3087  ordsucun 3089  unon 3095  ordunisuc 3096  0elsuc 3099  onuninsuc 3115  onun 3117  nlimsucg 3119  orduninsuc 3121  limsuc 3127  limuni3 3130  tfi 3133  tfis 3134  limomss 3144  limom 3153  findsg 3164  tfindsg 3169  opelxp1 3212  brrelex 3214  ralxp 3225  ralxpf 3227  elvvuni 3236  optocl 3242  onxpdisj 3248  ssrel 3254  xpsspw 3264  relop 3282  opelxpex2 3286  breldm 3322  dmsnop 3335  elreldm 3345  dmrnssfld 3364  dmcoss 3370  resabs1 3395  relimasn 3432  cnvsym 3444  xpnz 3473  xp11 3483  cores2 3514  coi2 3518  unixp0 3525  relcnvexb 3528  funsn 3550  funopg 3554  imadif 3581  f1ocnvb 3709  ffoss 3718  f1o00 3721  fo00 3722  fvprc 3728  tz6.12-1 3743  ssimaex 3775  fvopab4gf 3788  fvopabgf 3794  fvopabnf 3795  fvimacnv 3812  dffo4 3827  exfo 3829  fopabssxp 3831  rnssopab 3832  fopabsn 3847  fopabap 3848  fconst5 3855  abrexexlem1 3865  elunirnALT 3876  f1oweALT 3913  canth 3914  tfrlem4 3921  tfrlem5 3922  tfrlem7 3924  tfrlem8 3925  tfrlem9 3926  rdgsucopabn 3954  frsuct 3960  tz7.48lem 3962  tz7.48-1 3963  abianfplem 3968  abianfp 3969  oprabval2gf 4033  oprssdm 4049  ndmoprcom 4054  1stval2 4096  2ndval2 4097  unielxp 4114  eloprabi 4125  oaord 4188  nnacom 4240  nnmsucr 4247  nneob 4262  erref 4282  erthi 4288  ereldm 4292  erdisj 4293  ecelqsdm 4306  ectocl 4309  ecoptocl 4310  brecop2 4314  ecopoprdm 4316  th3qlem1 4321  mapprc 4333  mapsspm 4346  map0b 4350  map0 4351  ixpf 4363  uniixp 4364  idssen 4413  ener 4417  en0 4430  en1 4433  2dom 4434  snfi 4439  snfiOLD 4440  xpsnen 4442  xpdom2 4449  xpdom3 4452  pw2en 4453  sbthlem1 4454  sbthlem10 4463  domnsym 4470  domsdomtr 4483  pwuninel 4493  2pwuninel 4494  mapdom1 4499  mapdom2lem 4500  mapdom2 4501  mapxpen 4502  mapunen 4509  ssenen 4511  php 4520  php3 4522  0sdom1dom 4532  ominf 4538  ominfOLD 4539  isfinite1 4541  pssnn 4546  ssfi 4549  unfiOLD 4566  infcntss 4569  unifi 4572  unifiOLD 4574  fiint 4576  fiintOLD 4577  fodomfi 4582  fodomfiOLD 4583  pwfi 4586  pwfiOLD 4587  sucprcreg 4616  inf0 4622  inf3lem1 4629  infeq5 4637  dfom3 4646  trcl 4662  zfregs 4664  setind2 4666  r1tr 4671  r1val1 4675  tz9.12lem1 4676  tz9.12lem3 4678  rankr1 4691  rankel 4697  ranklim 4702  rankuni2 4707  rankun 4708  rankeq0 4713  rankr1id 4714  rankuni 4715  rankxpsuc 4732  scottex 4733  scott0 4734  bnd2 4741  karden 4743  hta 4745  aceq4 4751  aceq5lem4 4755  aceq5 4757  aceq6b 4759  ac7 4765  ac6lem 4771  ac6sf 4777  ac6s4 4778  kmlem2 4783  kmlem4 4785  kmlem12 4793  kmlem13 4794  weth 4804  zorn2lem6 4810  zorn2lem7 4811  zorn 4814  brdom5 4819  brdom4 4820  unidom 4825  sucdom 4859  sucdomOLD 4860  unxpdomlem 4861  carduni 4876  cardiun 4877  alephfp 4918  alephval2 4920  cardcf 4930  cfeq0 4933  cfsuc 4934  indpi 5053  prn0 5112  prpssnq 5113  1pr 5136  distrlem3pr 5148  prlem934b 5157  ltexprlem4 5164  reclem2pr 5176  mulcmpblnr 5202  recexsrlem 5231  map2psrpr 5239  suppsr3 5243  supsrlem2 5245  pre-axsup 5310  1re 5454  0re 5459  pnfnemnf 5555  xrltnrt 5560  addgegt0 5619  msqgt0 5632  redivcl 5807  prodgt0 5828  ltdiv2t 5896  sup3 6061  xrsupsslem 6085  xrinfmsslem 6086  xrsupss 6087  xrinfmss 6088  elnnz1 6164  znegclt 6172  elnn0nn 6180  zeot 6208  nn0ind 6221  nn0ind-raph 6223  qret 6267  qnegclt 6278  qrecclt 6281  om2uzran 6308  uzrdgval 6310  seq1lem1 6317  seq1suclem 6324  eluzelz 6431  eluzel2 6432  eluzle 6433  eluzaddi 6444  eluzsubi 6445  uzind4i 6462  elfzel2 6487  eluzfz1t 6495  seqzp1 6556  exple1t 6615  discrlem3 6666  discrlem 6667  nnesq 6670  sqrlem6 6686  sqrlem16 6696  sqrth 6707  sqrcl 6708  sqrge0 6710  cru 6745  crrecz 6749  negreb 6802  recvalz 6894  cjdiv 6895  cau3ir 6922  cau4i 6925  cau5 6926  cvg1i 6927  cvg1 6928  facnnt 6940  facp1t 6943  facnn2t 6946  faclbnd3 6954  faclbnd4lem1 6955  faclbnd4lem3 6957  bcpasc 6976  fsum1f 7014  fsump1f 7018  ser1ser0 7055  ser0mulc 7066  ser1mulc 7067  binomlem2 7074  binomlem3 7075  binomlem6 7078  binom 7079  clm4 7087  climaddlem2 7122  climmullem7 7133  climcmplem 7144  caucvglem2 7165  cvgcmpub 7192  isum1clim 7204  isumshft 7211  isumshft2 7212  expcnvlem2 7235  geosum 7248  cvgratlem2ALT 7255  fsum0diaglem2 7264  elcncf 7272  ivthlem2 7289  ivthlem6 7293  ivthlem7 7294  ivthlem9 7296  efaddlem26 7370  eftlexOLD 7384  efgt0 7411  eflt 7413  efcnlem2 7427  sin01bndlem2 7476  cos01bndlem2 7478  sin01gt0 7484  cos01gt0 7485  sin02gt0 7486  xpnnen 7507  ruclem33 7550  ruclem35 7552  infxpidmlem4 7563  infxpidmlem7 7566  infxpidmlem12 7571  infmap2lem1 7588  infmap2 7590  alephadd 7591  alephmul 7592  alephexp1 7593  alephsuc3 7594  alephexp2 7595  sn0top 7651  indistop 7652  distop 7653  ntrss2 7694  qdensere 7755  cnpco 7773  msflem 7807  lpbl 7884  tgioo 7919  dscmet 7922  lmle 7964  metelcls 7969  metcnp4 7974  fsumcnlem 7993  iscms2 7998  bcthlem4 8006  bcthlem14 8016  bcthlem22 8024  grpsn 8127  ablmul 8134  ringi 8145  ringsn 8166  vci 8170  nvi 8236  nvoprne 8309  ipfval 8355  nmobndseqi 8443  phpar2 8485  ipasslem5 8497  ubthlem6 8537  minveclem10 8557  minveclem14 8561  spwmo 8659  pilem2 8674  sincosq1sgn 8706  sincosq2sgn 8707  sincosq3sgn 8708  sincosq4sgn 8709  sinq12gt0t 8710  cosh111lem1 8716  efifolem5 8728  circgrp 8742  shftefif1olem 8743  effoi 8747  hvsubeq0 8932  hvmulcant 8941  hvmulcan2t 8942  bcsALT 9048  chsscm 9114  chcmh 9115  hsn0elch 9122  hhssnv 9136  projlem8 9195  projlem13 9200  shintcl 9295  spanvalt 9301  dfchj2 9326  sshjclt 9329  shsidm 9359  spanun 9469  h1de2 9478  spansn 9482  spanunsn 9504  cmbr3 9545  osumlem1 9580  osumlem2 9581  osumlem3 9582  osumcor2 9592  spansncv 9599  5oalem7 9607  3oalem3 9611  pjss2 9627  pjssm 9628  mayete3 9675  nmop0h 9918  lnopcon 9965  lnfncon 9992  riesz3 9997  nmopco 10030  pjnmop 10077  pjorthco 10099  pjssdif1 10105  elpjcht 10119  pjin2 10124  pjclem1 10126  pjclem2 10127  pjclem4a 10129  pj3lem1 10137  hstclt 10147  hst1t 10148  hstel2t 10149  strlem1 10180  strlem3 10183  strlem4 10184  strlem5 10185  str 10187  hstrlem3 10191  hstrlem4 10192  hstrlem5 10193  hstr 10195  stcltr1 10204  dmdbr5 10238  mdsl1 10251  mdslmd1lem2 10256  atn0 10275  atom1d 10283  shatomic 10288  chrelat2 10295  atssmat 10308  irred 10324  cmmd 10346  sumdmd 10350  dmdbr4at 10351  dmdbr5at 10352  dmdbr6at 10353  dmdbr7at 10354  cdj3lem1 10364  ghomgrpilem2 10389  symggrpi 10409  r19.3rzvb 10440  uninqs 10444  infi1 10449  ficli 10470  inposet 10485  mapdiscn 10505  cmphmp 10515  top2ind 10542  top2usne 10543  homindlem3 10545  qusp 10549  fgsb 10563  efilcp 10564  infi 10567  fgsb2 10568  efilcp2 10569  cnfilca 10570  rcfpfillem3 10573  rcfpfillem4 10574  rcfpfillem6 10576  rcfpfil 10577  algi 10639  dedi 10649  cati 10667  0ded 10669  0cat 10670  imonclem 10720  hgralem 10749

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

This theorem depends on definitions:  df-bi 147

Copyright terms: Public domain