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 579  ordi 596  pm5.18 660  ccase 755  3simpb 786  3simpc 787  3imp 827  3com13 838  syl3anb 869  a6e 990  19.33b 1092  exintrbi 1118  equvini 1168  sb6x 1188  equs5e 1198  hbsb4t 1249  a12stdy2 1373  a12lem2 1377  euex 1394  eumo0 1395  mooran2 1426  mopick 1433  euor2 1437  2euex 1441  2mo 1447  2eu3 1451  exists2 1458  eqcoms 1478  necon3ai 1606  necon1ai 1608  rexex 1693  ra4 1694  r19.20 1702  r19.22 1731  r19.23ai 1742  r19.36av 1760  r19.37av 1761  r19.44av 1766  r19.45av 1767  elisset 1817  gencl 1828  vtoclgf 1846  cla4gf 1860  rcla4 1871  mo2icl 1923  moi2 1924  moi 1925  reu6 1932  2reuswap 1937  ra4sbc 1997  ra5 2000  sstr2 2071  pssn2lp 2147  ssnpss 2149  unineq 2255  reuun2 2278  disjssun 2326  pssnel 2331  difin0ss 2332  r19.2z 2347  r19.3rzv 2348  ralidm 2357  ifbi 2371  prprc1 2452  pwpw0 2469  sspr 2475  snsssn 2478  preqr2 2482  preq12b 2483  opthpr 2485  opprc1 2498  pwsnALT 2501  intmin4 2559  iunconst 2572  ssiun 2592  iununi 2616  trss 2689  axrep5 2698  zfrep4 2701  ssex 2719  intex 2729  intnex 2730  intabs 2733  snex 2750  rext 2754  unipw 2756  sspwuni 2758  moabex 2766  nnullss 2768  exss 2769  axpr 2778  opth 2787  copsexg 2792  opprc3 2797  ssopab2 2822  pwssun 2827  solin 2857  euuni 2881  reucl 2885  reuunisn 2895  reuxfr 2904  reuunixfr 2906  elpwunsn 2912  frc 2920  frirr 2924  fr2nr 2925  fr3nr 2926  onfr 2986  nlim0 3027  limord 3028  limuni 3029  elsuci 3035  sucprc 3044  onmindif2 3061  suceloni 3062  ordpwsuc 3066  onsucmin 3072  ordsucelsuc 3073  ordssun 3079  ordequn 3080  ordsucun 3082  unon 3088  ordunisuc 3089  0elsuc 3092  onuninsuc 3108  onun 3110  nlimsucg 3112  orduninsuc 3114  limsuc 3120  limuni3 3123  tfi 3126  tfis 3127  limomss 3137  limom 3146  findsg 3157  tfindsg 3162  opelxp1 3205  brrelex 3207  ralxp 3218  ralxpf 3220  elvvuni 3229  optocl 3235  onxpdisj 3241  ssrel 3247  xpsspw 3257  relop 3275  opelxpex2 3279  breldm 3315  dmsnop 3328  elreldm 3338  dmrnssfld 3357  dmcoss 3363  resabs1 3388  relimasn 3425  cnvsym 3437  xpnz 3466  xp11 3476  cores2 3507  coi2 3511  unixp0 3518  relcnvexb 3521  funsn 3543  funopg 3547  imadif 3574  f1ocnvb 3702  ffoss 3711  f1o00 3714  fo00 3715  fvprc 3721  tz6.12-1 3736  ssimaex 3768  fvopab4gf 3781  fvopabgf 3787  fvopabnf 3788  fvimacnv 3805  dffo4 3820  exfo 3822  fopabssxp 3824  rnssopab 3825  fopabsn 3840  fopabap 3841  fconst5 3848  abrexexlem1 3858  elunirnALT 3869  f1oweALT 3906  canth 3907  tfrlem4 3914  tfrlem5 3915  tfrlem7 3917  tfrlem8 3918  tfrlem9 3919  rdgsucopabn 3947  frsuct 3953  tz7.48lem 3955  tz7.48-1 3956  abianfplem 3961  abianfp 3962  oprabval2gf 4026  oprssdm 4042  ndmoprcom 4047  1stval2 4089  2ndval2 4090  unielxp 4107  eloprabi 4118  oaord 4181  nnacom 4233  nnmsucr 4240  nneob 4255  erref 4275  erthi 4281  ereldm 4285  erdisj 4286  ecelqsdm 4299  ectocl 4302  ecoptocl 4303  brecop2 4307  ecopoprdm 4309  th3qlem1 4314  mapprc 4326  mapsspm 4339  map0b 4343  map0 4344  ixpf 4356  uniixp 4357  idssen 4406  ener 4410  en0 4423  en1 4426  2dom 4427  snfi 4432  snfiOLD 4433  xpsnen 4435  xpdom2 4442  xpdom3 4445  pw2en 4446  sbthlem1 4447  sbthlem10 4456  domnsym 4463  domsdomtr 4476  pwuninel 4486  2pwuninel 4487  mapdom1 4492  mapdom2lem 4493  mapdom2 4494  mapxpen 4495  mapunen 4502  ssenen 4504  php 4513  php3 4515  0sdom1dom 4525  ominfOLD 4529  pssnn 4534  ssfi 4537  unfiOLD 4552  infcntss 4554  unifiOLD 4557  fiint 4559  fiintOLD 4560  abfii4OLD 4564  fodomfiOLD 4566  pwfiOLD 4571  sucprcreg 4600  inf0 4606  inf3lem1 4613  infeq5 4621  dfom3 4630  trcl 4645  zfregs 4647  setind2 4649  r1tr 4654  r1val1 4658  tz9.12lem1 4659  tz9.12lem3 4661  rankr1 4674  rankel 4680  ranklim 4685  rankuni2 4690  rankun 4691  rankeq0 4696  rankr1id 4697  rankuni 4698  rankxpsuc 4715  scottex 4716  scott0 4717  bnd2 4724  karden 4726  hta 4728  aceq4 4734  aceq5lem4 4738  aceq5 4740  aceq6b 4742  ac7 4748  ac6lem 4754  ac6sf 4760  ac6s4 4761  kmlem2 4766  kmlem4 4768  kmlem12 4776  kmlem13 4777  weth 4787  zorn2lem6 4793  zorn2lem7 4794  zorn 4797  brdom5 4802  brdom4 4803  unidom 4808  sucdom 4842  unxpdomlem 4843  carduni 4858  cardiun 4859  alephfp 4900  alephval2 4902  cardcf 4911  cfeq0 4914  cfsuc 4915  indpi 5034  prn0 5093  prpssnq 5094  1pr 5117  distrlem3pr 5129  prlem934b 5138  ltexprlem4 5145  reclem2pr 5157  mulcmpblnr 5183  recexsrlem 5212  map2psrpr 5220  suppsr3 5224  supsrlem2 5226  pre-axsup 5291  1re 5435  0re 5440  pnfnemnf 5536  xrltnrt 5541  addgegt0 5600  msqgt0 5613  redivcl 5798  prodgt0 5819  ltdiv2t 5887  sup3 6052  xrsupsslem 6076  xrinfmsslem 6077  xrsupss 6078  xrinfmss 6079  elnnz1 6155  znegclt 6163  elnn0nn 6171  zeot 6199  nn0ind 6212  nn0ind-raph 6214  qret 6259  qnegclt 6270  qrecclt 6273  om2uzran 6300  uzrdgval 6302  seq1lem1 6309  seq1suclem 6316  eluzelz 6423  eluzel2 6424  eluzle 6425  eluzaddi 6436  eluzsubi 6437  uzind4i 6454  elfzel2 6479  eluzfz1t 6487  seqzp1 6548  exple1t 6607  discrlem3 6658  discrlem 6659  nnesq 6662  sqrlem6 6678  sqrlem16 6688  sqrth 6699  sqrcl 6700  sqrge0 6702  cru 6737  crrecz 6741  negreb 6795  recvalz 6887  cjdiv 6888  cau3ir 6915  cau4i 6918  cau5 6919  cvg1i 6920  cvg1 6921  facnnt 6933  facp1t 6936  facnn2t 6939  faclbnd3 6947  faclbnd4lem1 6948  faclbnd4lem3 6950  bcpasc 6969  fsum1f 7007  fsump1f 7011  ser1ser0 7048  ser0mulc 7059  ser1mulc 7060  binomlem2 7067  binomlem3 7068  binomlem6 7071  binom 7072  clm4 7080  climaddlem2 7115  climmullem7 7126  climcmplem 7137  caucvglem2 7158  cvgcmpub 7185  isum1clim 7197  isumshft 7204  isumshft2 7205  expcnvlem2 7228  geosum 7241  cvgratlem2ALT 7248  fsum0diaglem2 7257  elcncf 7265  ivthlem2 7282  ivthlem6 7286  ivthlem7 7287  ivthlem9 7289  efaddlem26 7363  eftlexOLD 7377  efgt0 7404  eflt 7406  efcnlem2 7420  sin01bndlem2 7468  cos01bndlem2 7470  sin01gt0 7476  cos01gt0 7477  sin02gt0 7478  xpnnen 7499  ruclem33 7542  ruclem35 7544  infxpidmlem4 7555  infxpidmlem7 7558  infxpidmlem12 7563  infmap2lem1 7579  infmap2 7581  alephadd 7582  alephmul 7583  alephexp1 7584  alephsuc3 7585  alephexp2 7586  subbasOLD 7644  subbas2OLD 7645  sn0top 7647  indistop 7648  distop 7649  ntrss2 7690  qdensere 7751  cnpco 7769  msflem 7803  lpbl 7880  tgioo 7915  dscmet 7918  lmle 7960  metelcls 7965  metcnp4 7970  fsumcnlem 7989  iscms2 7994  bcthlem4 8002  bcthlem14 8012  bcthlem22 8020  grpsn 8124  ablmul 8131  ringi 8142  ringsn 8163  vci 8167  nvi 8233  nvoprne 8306  ipfval 8352  nmobndseqi 8440  phpar2 8482  ipasslem5 8494  ubthlem6 8534  minveclem10 8554  minveclem14 8558  spwmo 8656  pilem2 8672  sincosq1sgn 8704  sincosq2sgn 8705  sincosq3sgn 8706  sincosq4sgn 8707  sinq12gt0t 8708  cosh111lem1 8714  efifolem5 8726  circgrp 8740  shftefif1olem 8741  effoi 8745  hvsubeq0 8930  hvmulcant 8939  hvmulcan2t 8940  bcsALT 9046  chsscm 9112  chcmh 9113  hsn0elch 9120  hhssnv 9134  projlem8 9193  projlem13 9198  shintcl 9293  spanvalt 9299  dfchj2 9324  sshjclt 9327  shsidm 9357  spanun 9467  h1de2 9476  spansn 9480  spanunsn 9502  cmbr3 9543  osumlem1 9578  osumlem2 9579  osumlem3 9580  osumcor2 9590  spansncv 9597  5oalem7 9605  3oalem3 9609  pjss2 9625  pjssm 9626  mayete3 9673  nmop0h 9916  lnopcon 9963  lnfncon 9990  riesz3 9995  nmopco 10028  pjnmop 10075  pjorthco 10097  pjssdif1 10103  elpjcht 10116  pjin2 10121  pjclem1 10123  pjclem2 10124  pjclem4a 10126  pj3lem1 10134  hstclt 10144  hst1t 10145  hstel2t 10146  strlem1 10177  strlem3 10180  strlem4 10181  strlem5 10182  str 10184  hstrlem3 10188  hstrlem4 10189  hstrlem5 10190  hstr 10192  stcltr1 10201  dmdbr5 10235  mdsl1 10248  mdslmd1lem2 10253  atn0 10272  atom1d 10280  shatomic 10285  chrelat2 10292  atssmat 10305  irred 10321  cmmd 10343  sumdmd 10347  dmdbr4at 10348  dmdbr5at 10349  dmdbr6at 10350  dmdbr7at 10351  cdj3lem1 10361  ghomgrpilem2 10386  symggrpi 10406  r19.3rzvb 10437  uninqs 10441  infi1 10447  infi1OLD 10448  ficli 10472  ficliOLD 10473  mapdiscn 10511  cmphmp 10521  sfseqeq 10543  top2ind 10548  top2usne 10549  homindlem3 10551  qusp 10555  fgsb 10570  fgsbOLD 10571  efilcp 10572  efilcpOLD 10573  infi 10578  infiOLD 10579  fgsb2 10580  efilcp2 10581  efilcp2OLD 10582  cnfilca 10583  cnfilcaOLD 10584  rcfpfillem2OLD 10588  rcfpfillem3 10589  rcfpfillem3OLD 10590  rcfpfillem4 10591  rcfpfillem4OLD 10592  rcfpfillem6 10595  rcfpfillem6OLD 10596  rcfpfil 10597  rcfpfilOLD 10598  algi 10660  dedi 10670  cati 10688  0ded 10690  0cat 10691  imonclem 10741  hgralem 10770

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