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 436  an1s 486  an1rs 489  an4s 508  pm2.85 578  ordi 595  pm5.18 659  ccase 754  3simpb 785  3simpc 786  3imp 826  3com13 837  syl3anb 868  a6e 988  19.33b 1090  exintrbi 1116  equvini 1166  sb6x 1186  equs5e 1196  hbsb4t 1247  a12stdy2 1371  a12lem2 1375  euex 1392  eumo0 1393  mooran2 1424  mopick 1431  euor2 1435  2euex 1439  2mo 1445  2eu3 1449  exists2 1456  eqcoms 1475  necon3ai 1603  necon1ai 1605  rexex 1690  ra4 1691  r19.20 1699  r19.22 1728  r19.23ai 1739  r19.36av 1757  r19.37av 1758  r19.44av 1763  r19.45av 1764  elisset 1813  gencl 1824  vtoclgf 1842  cla4gf 1856  rcla4 1867  mo2icl 1919  moi2 1920  moi 1921  reu6 1928  2reuswap 1933  ra4sbc 1993  ra5 1996  sstr2 2067  pssn2lp 2143  ssnpss 2145  unineq 2251  reuun2 2274  disjssun 2322  pssnel 2327  difin0ss 2328  r19.2z 2343  r19.3rzv 2344  ralidm 2353  ifbi 2367  prprc1 2448  pwpw0 2465  sspr 2471  snsssn 2474  preqr2 2478  preq12b 2479  opthpr 2481  opprc1 2494  intmin4 2554  iunconst 2567  ssiun 2587  iununi 2611  trss 2684  axrep5 2693  zfrep4 2696  ssex 2714  intex 2724  intnex 2725  intabs 2728  snex 2745  rext 2749  unipw 2751  sspwuni 2753  moabex 2761  nnullss 2763  exss 2764  axpr 2773  opth 2782  copsexg 2787  opprc3 2792  ssopab2 2817  pwssun 2822  solin 2852  euuni 2876  reucl 2880  reuunisn 2890  reuxfr 2899  reuunixfr 2901  elpwunsn 2907  frc 2915  frirr 2919  fr2nr 2920  fr3nr 2921  onfr 2981  nlim0 3022  limord 3023  limuni 3024  elsuci 3030  sucprc 3039  onmindif2 3056  suceloni 3057  ordpwsuc 3061  onsucmin 3067  ordsucelsuc 3068  ordssun 3074  ordequn 3075  ordsucun 3077  unon 3083  ordunisuc 3084  0elsuc 3087  onuninsuc 3103  onun 3105  nlimsucg 3107  orduninsuc 3109  limsuc 3115  limuni3 3118  tfi 3121  tfis 3122  limomss 3132  limom 3141  findsg 3152  tfindsg 3157  opelxp1 3200  brrelex 3202  ralxp 3213  ralxpf 3215  elvvuni 3224  optocl 3230  onxpdisj 3236  ssrel 3242  xpsspw 3252  relop 3270  opelxpex2 3274  breldm 3310  dmsnop 3323  elreldm 3333  dmrnssfld 3351  dmcoss 3355  resabs1 3380  relimasn 3417  cnvsym 3429  xpnz 3458  xp11 3468  cores2 3499  coi2 3503  unixp0 3510  relcnvexb 3513  funsn 3535  funopg 3539  imadif 3566  f1ocnvb 3693  ffoss 3702  f1o00 3705  fo00 3706  fvprc 3712  tz6.12-1 3727  ssimaex 3759  fvopab4gf 3772  fvopabgf 3778  fvopabnf 3779  fvimacnv 3796  dffo4 3811  exfo 3813  fopabssxp 3815  rnssopab 3816  fopabsn 3831  fopabap 3832  fconst5 3839  abrexexlem1 3849  elunirnALT 3860  f1oweALT 3897  canth 3898  tfrlem4 3905  tfrlem5 3906  tfrlem7 3908  tfrlem8 3909  tfrlem9 3910  rdgsucopabn 3938  frsuct 3944  tz7.48lem 3946  tz7.48-1 3947  abianfplem 3952  abianfp 3953  oprabval2gf 4017  oprssdm 4033  ndmoprcom 4039  1stval2 4079  2ndval2 4080  unielxp 4097  eloprabi 4108  oaord 4171  nnacom 4223  nnmsucr 4230  nneob 4245  erref 4265  erthi 4271  ereldm 4275  erdisj 4276  ecelqsdm 4289  ectocl 4292  ecoptocl 4293  brecop2 4297  ecopoprdm 4299  th3qlem1 4304  mapprc 4316  mapsspm 4329  map0b 4333  map0 4334  ixpf 4346  uniixp 4347  idssen 4393  ener 4397  en0 4410  en1 4413  2dom 4414  snfi 4419  xpsnen 4421  xpdom2 4428  xpdom3 4431  pw2en 4432  sbthlem1 4433  sbthlem10 4442  domnsym 4449  domsdomtr 4462  pwuninel 4472  2pwuninel 4473  mapdom1 4478  mapdom2lem 4479  mapdom2 4480  mapxpen 4481  mapunen 4488  ssenen 4490  php 4499  0sdom1dom 4510  ominf 4514  pssnn 4519  unfi 4534  infcntss 4536  unifi 4538  fiint 4540  abfii4 4544  fodomfi 4546  pwfi 4551  sucprcreg 4580  inf0 4586  inf3lem1 4593  infeq5 4601  dfom3 4610  trcl 4625  zfregs 4627  setind2 4629  r1tr 4634  r1val1 4638  tz9.12lem1 4639  tz9.12lem3 4641  rankr1 4654  rankel 4660  ranklim 4665  rankuni2 4670  rankun 4671  rankeq0 4676  rankr1id 4677  rankuni 4678  rankxpsuc 4695  scottex 4696  scott0 4697  bnd2 4704  karden 4706  hta 4708  aceq4 4714  aceq5lem4 4718  aceq5 4720  aceq6b 4722  ac7 4728  ac6lem 4734  ac6sf 4740  ac6s4 4741  kmlem2 4746  kmlem4 4748  kmlem12 4756  kmlem13 4757  weth 4767  zorn2lem6 4773  zorn2lem7 4774  zorn 4777  brdom5 4782  brdom4 4783  unidom 4788  sucdom 4822  unxpdomlem 4823  carduni 4838  cardiun 4839  alephfp 4880  alephval2 4882  cardcf 4891  cfeq0 4894  cfsuc 4895  indpi 5014  prn0 5073  prpssnq 5074  1pr 5097  distrlem3pr 5109  prlem934b 5118  ltexprlem4 5125  reclem2pr 5137  mulcmpblnr 5163  recexsrlem 5192  map2psrpr 5200  suppsr3 5204  supsrlem2 5206  pre-axsup 5271  1re 5415  0re 5420  pnfnemnf 5517  xrltnrt 5522  addgegt0 5582  msqgt0 5595  redivcl 5762  prodgt0 5783  ltdiv2t 5843  sup3 6007  xrsupsslem 6031  xrinfmsslem 6032  xrsupss 6033  xrinfmss 6034  elnnz1 6110  znegclt 6118  elnn0nn 6126  zeot 6154  nn0ind 6168  nn0ind-raph 6170  qret 6205  qnegclt 6216  qrecclt 6219  om2uzran 6245  uzrdgval 6247  seq1lem1 6254  seq1suclem 6261  eluzelz 6363  eluzel2 6364  eluzle 6365  eluzaddi 6376  eluzsubi 6377  uzind4i 6394  elfzel2 6419  eluzfz1t 6427  seqzp1 6488  exple1t 6546  discrlem3 6596  discrlem 6597  nnesq 6600  sqrlem6 6616  sqrlem16 6626  sqrth 6637  sqrcl 6638  sqrge0 6640  cru 6675  crrecz 6680  rereb 6723  negreb 6738  recvalz 6833  cjdiv 6834  cau3ir 6860  cau4i 6863  cau5 6864  cvg1i 6865  cvg1 6866  facnnt 6878  facp1t 6881  facnn2t 6884  faclbnd3 6892  faclbnd4lem1 6893  faclbnd4lem3 6895  bcpasc 6915  fsum1f 6953  fsump1f 6957  ser1ser0 6994  ser0mulc 7005  ser1mulc 7006  binomlem2 7013  binomlem3 7014  binomlem6 7017  binom 7018  clm4 7026  climaddlem2 7059  climmullem7 7070  climcmplem 7081  caucvglem2 7102  cvgcmpub 7129  isumshft 7147  isumshft2 7148  expcnvlem2 7171  geosum 7184  cvgratlem2ALT 7191  fsum0diaglem2 7200  elcncf 7208  ivthlem2 7225  ivthlem6 7229  ivthlem7 7230  ivthlem9 7232  ivthlem6OLD 7238  ivthlem7OLD 7239  efaddlem26 7313  eftlexOLD 7327  efgt0 7353  eflt 7355  efcnlem2 7368  sin01bndlem2 7418  cos01bndlem2 7420  sin01gt0 7426  cos01gt0 7427  sin02gt0 7428  xpnnen 7449  ruclem33 7493  ruclem35 7495  infxpidmlem4 7506  infxpidmlem7 7509  infxpidmlem12 7514  infmap2lem1 7529  infmap2 7531  alephadd 7532  alephmul 7533  alephexp1 7534  alephsuc3 7535  alephexp2 7536  subbas 7594  subbas2 7595  sn0top 7597  indistop 7598  distop 7599  ntrss2 7640  qdensere 7701  cnpco 7719  msflem 7753  lpbl 7832  tgioo 7867  dscmet 7870  lmle 7911  metelcls 7916  metcnp4 7920  fsumcnlem 7939  iscms2 7944  bcthlem4 7952  bcthlem14 7962  bcthlem22 7970  grpsn 8076  ablmul 8083  ringi 8094  ringsn 8115  vci 8119  nvi 8185  ipfval 8299  nmobndseqi 8385  phpar2 8426  ipasslem5 8438  ubthlem6 8478  minveclem10 8498  minveclem14 8502  spwmo 8598  pilem2 8610  sincosq1sgn 8640  sincosq2sgn 8641  sincosq3sgn 8642  sincosq4sgn 8643  sinq12gt0t 8644  cosh111lem1 8648  efifolem5 8660  circgrp 8679  shftefif1olem 8680  effoi 8684  hvsubeq0 8869  hvmulcant 8878  hvmulcan2t 8879  bcsALT 8985  chsscm 9051  chcmh 9052  hsn0elch 9059  hhssnv 9073  projlem8 9132  projlem13 9137  shintcl 9231  spanvalt 9237  dfchj2 9262  sshjclt 9265  shsidm 9295  spanun 9405  h1de2 9414  spansn 9419  spanunsn 9442  cmbr3 9483  osumlem1 9518  osumlem2 9519  osumlem3 9520  osumcor2 9530  spansncv 9537  5oalem7 9545  3oalem3 9549  pjss2 9565  pjssm 9566  mayete3 9613  nmop0h 9854  lnopcon 9901  lnfncon 9928  riesz3 9933  nmopco 9966  pjnmop 10013  pjorthco 10035  pjssdif1 10041  elpjcht 10054  pjin2 10059  pjclem1 10061  pjclem2 10062  pjclem4a 10064  pj3lem1 10072  hstclt 10082  hst1t 10083  hstel2t 10084  strlem1 10115  strlem3 10118  strlem4 10119  strlem5 10120  str 10122  hstrlem3 10126  hstrlem4 10127  hstrlem5 10128  hstr 10130  stcltr1 10139  mdsl1 10185  mdslmd1lem2 10190  atn0 10209  atom1d 10217  shatomic 10222  chrelat2 10229  atssmat 10242  irred 10258  cmmd 10279  sumdmd 10283  dmdbr5at 10284  dmdbr6at 10285  cdj3lem1 10295  ghomgrpilem2 10320  symggrpi 10340  r19.3rzvb 10373  uninqs 10378  infi1 10383  ficli 10404  mapdiscn 10434  cmphmp 10444  qusp 10466  fgsb 10480  efilcp 10481  infi 10484  fgsb2 10485  efilcp2 10486  cnfilca 10487  algi 10540  dedi 10550  cati 10568  0ded 10570  0cat 10571  imonclem 10619  hgralem 10642

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