Theorem sylbi 216

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	biimpi 168	. 2 |- (ph -> ps)
3		sylbi.2	. 2 |- (ps -> ch)
4	2, 3	syl 12	1 |- (ph -> ch)

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

This theorem is referenced by:  3imtr4i 236  simpl 346  simpr 350  ancoms 484  an1s 544  an1rs 547  an4s 566  pm2.85 639  ordiOLD 657  pm5.18 722  pm5.18OLD 723  ccase 829  dn1OLD 856  3simpb 873  3simpc 874  3simpcOLD 875  3imp 1061  3com12 1071  3com13 1073  syl3anb 1140  a6e 1336  19.33b 1444  19.33bOLD 1445  exintrbi 1476  equvini 1531  equviniOLD 1532  sb6xOLD 1554  equs5e 1567  sbf3t 1619  hbsb4tOLD 1622  a12stdy2 1764  a12lem2 1768  euex 1788  euexOLD 1789  eumo0 1790  mooran2OLD 1825  mopick 1833  euor2OLD 1840  2euex 1844  2euexOLD 1845  2mo 1851  2eu3 1855  exists2 1863  exists2OLD 1864  eqcoms 1887  eleq2s 1983  necon3aiOLD 2044  necon3bi 2045  necon1ai 2047  necon2ai 2051  pm2.61ne 2087  pm2.61ine 2089  rexex 2154  ra4 2155  ralim 2164  reximOLD 2195  r19.23aiOLD 2210  r19.36av 2232  r19.37av 2233  r19.44av 2240  r19.45av 2241  elissetOLD 2300  gencl 2318  gencbvex 2334  vtoclgf 2345  cla4gf 2361  cla4gfOLD 2363  rcla4OLD 2374  mo2icl 2434  moi2 2435  moi 2436  reu3 2444  2reuswap 2449  ra4sbc 2536  ra5 2539  csbhypf 2572  sstr2OLD 2624  sseq1 2637  pssn2lpOLD 2710  ssnpssOLD 2713  unineq 2844  reuun2 2873  reldisj 2916  disjssunOLD 2933  pssnel 2938  difin0ss 2939  r19.2z 2958  r19.3rz 2960  r19.3rzv 2962  ralidm 2973  ifbi 2995  prprc1 3108  difprsn 3127  pwpw0 3134  sspr 3144  snsssn 3148  preqr2 3153  preq12b 3154  opthpr 3156  opprc1 3170  pwsnALT 3173  reucl 3213  elinti 3223  unissintOLD 3242  intmin4 3246  iunconstOLD 3263  dfiin2g 3286  ssiunOLD 3294  iununiOLD 3332  trel 3418  trss 3421  axrep5 3433  zfrep4 3436  ssex 3455  intex 3465  intnex 3466  intabs 3469  abssexg 3490  snexOLD 3493  rext 3502  unipw 3504  moabex 3513  nnullss 3515  exss 3516  axpr 3523  opth 3532  copsexg 3537  copsexgOLD 3538  opprc3 3543  ssopab2 3573  pwssun 3578  solin 3612  frc 3629  frirr 3634  fr2nr 3635  onfr 3702  elsuci 3731  sucprc 3740  ordsssuc2 3758  ordssun 3769  ordequn 3770  onun2i 3785  euuni 3807  reuuni1 3808  reuunisn 3822  eualeqhb 3824  euexeqOLD 3826  euexaleq 3827  eufromeq1 3828  eufromeq3 3830  eufromeq5 3832  euobj1 3834  euobj2 3835  reuxfrd 3846  reuunixfr 3850  elpwunsn 3856  fr3nr 3859  onmindif2 3893  suceloni 3894  ordpwsuc 3896  onsucmin 3901  ordsucelsuc 3902  ordsucelsucOLD 3903  ordsucun 3905  unon 3910  ordunisuc 3911  ordunisucOLD 3912  0elsuc 3916  onuninsuci 3921  nlimsucgOLD 3924  orduninsuc 3925  limsuc 3933  limuni3 3936  tfi 3937  tfis 3938  tfindsg 3944  limomss 3956  limom 3967  find 3977  findsg 3980  opelxp1 4026  brrelex 4028  ralxp 4041  ralxpf 4043  elvvuni 4055  optocl 4061  0nelelxp 4067  onxpdisjOLD 4069  ssrelOLD 4076  xpsspw 4093  relop 4113  opelxpex2 4119  opelxpex2OLD 4120  breldm 4161  elreldm 4185  dmrnssfld 4205  dmcossOLD 4212  dmcosseq 4214  resabs1 4244  relimasn 4288  cnvsymOLD 4305  asymref 4308  asymref2 4310  xpnz 4335  xp11 4347  xpcan 4348  xpcan2 4350  dmsnop 4367  dmsnopOLD 4368  dfco2a 4394  dfco2aOLD 4395  cores2 4410  coi2 4414  unixp0 4423  relcnvexb 4426  dffun8 4448  funopg 4454  funsnOLD 4464  imadif 4493  fneu 4517  fcoi1 4584  fcoi2 4586  f1ocnv 4651  f1ocnvb 4653  ffoss 4665  f1o00 4668  fo00 4669  fvprc 4678  tz6.12-1 4693  nfunsn 4706  nfunsnOLD 4707  ssimaex 4729  dffv2 4734  fvimacnv 4778  dffo4 4793  exfo 4795  fopabssxp 4797  rnssopab 4798  fopabsnOLD 4816  fopabap 4817  fconst5 4824  abrexexlem1 4834  elunirnALT 4845  f1oweALT 4883  oprssdm 4975  ndmoprcom 4980  1stval2 5030  2ndval2 5031  fo1stres 5036  fo2ndres 5037  1st2val 5038  2nd2val 5039  unielxp 5047  dfoprab5sf 5058  eloprabi 5060  iotaequ 5097  iotanul 5098  iota4 5100  reiotacl2 5105  reiota1 5108  canth 5112  tfrlem4 5122  tfrlem5 5123  tfrlem7 5125  tfrlem8 5126  tfrlem9 5127  rdgsucopabn 5155  frsuc 5161  tz7.48lem 5164  tz7.48-1 5165  abianfp 5171  oaord 5228  nnacom 5288  nnmsucrOLD 5296  nneob 5312  erref 5333  erthi 5339  ereldm 5343  erdisj 5344  ecelqsdm 5358  ectocl 5361  ecoptocl 5362  brecop2 5366  ecopoprdm 5368  th3qlem1 5373  mapprc 5385  mapsspm 5398  map0b 5402  map0 5403  ixpf 5415  uniixp 5416  idssen 5465  ener 5469  en0 5482  en1 5485  2dom 5486  snfi 5491  xpsnen 5494  xpdom2 5501  xpdom3 5504  pw2en 5505  ac6sfi 5509  sbthlem1 5510  sbthlem10 5519  domnsym 5526  domsdomtr 5539  pwuninel 5550  2pwuninel 5551  riotav 5565  riotaprc 5567  riotauni 5568  mapdom1 5586  mapdom2lem 5587  mapdom2 5588  mapxpen 5589  mapunen 5596  ssenen 5598  php 5607  php3 5609  0sdom1dom 5618  ominf 5622  isfinite1 5624  pssnn 5628  ssfi 5630  infcntss 5646  unifi 5648  fiint 5650  abfii4 5654  fodomfi 5656  pwfi 5661  hartoglem 5692  hartog 5693  sucprcreg 5703  inf0 5712  inf3lem1 5719  infeq5 5727  dfom3 5737  trcl 5752  zfregs 5754  setind2 5760  r1tr 5765  r1val1 5769  tz9.12lem1 5770  tz9.12lem3 5772  rankr1 5785  rankel 5791  ranklim 5796  rankuni2 5801  rankun 5802  rankeq0 5807  rankr1id 5808  rankuni 5809  rankxpsuc 5826  scottex 5846  scott0 5847  bnd2 5854  karden 5856  hta 5858  aceq4 5896  aceq5lem4 5900  aceq5 5902  aceq6b 5904  ac7 5910  ac6lem 5916  ac6sf 5922  ac6s4 5923  kmlem2 5928  kmlem4 5930  kmlem12 5938  kmlem13 5939  weth 5949  zorn2lem6 5955  zorn2lem7 5956  zorn 5959  brdom5 5964  brdom4 5965  unidom 5970  sucdom 5994  unxpdomlem 5995  carduni 6010  cardiun 6011  alephfp 6048  alephval2 6050  cardcf 6059  cfeq0 6062  cfsuc 6063  nnaun 6089  indpi 6186  prn0 6245  prpssnq 6246  1pr 6269  distrlem3pr 6281  prlem934b 6290  ltexprlem4 6297  reclem2pr 6309  mulcmpblnr 6335  recexsrlem 6364  map2psrpr 6372  suppsr3 6376  supsrlem2 6378  pre-axsup 6444  1re 6598  0re 6603  renfdisj 6712  xrltnr 6716  addgegt0iOLD 6780  msqgt0i 6794  redivcli 6976  prodgt0i 6997  ltdiv2 7070  sup3 7261  xrsupsslem 7285  xrinfmsslem 7286  xrsupss 7287  xrinfmss 7288  elnnz1 7364  znegcl 7372  elnn0nn 7380  zeo 7411  nn0ind 7424  nn0ind-raph 7426  qre 7439  qnegcl 7450  qreccl 7453  eluzaddi 7605  eluzsubi 7606  uzind4i 7623  elfzel2i 7649  eluzfz1 7657  om2uzrani 7711  uzrdgvali 7714  cardfz 7719  seq1lem1 7722  seq1suclem 7729  seqzp1 7791  exple1 7852  discrlem3 7908  discrlem 7909  nnesqi 7912  nn0opthlem2 7915  nn0opthi 7916  sqrlem6 7928  sqrlem16 7938  sqrthi 7949  sqrcli 7950  sqrge0i 7952  crui 7987  crreczi 7991  negrebi 8045  recvalzi 8139  cjdivi 8140  cau3iri 8167  cau4ii 8170  cau5i 8171  cvg1i 8172  cvg1 8173  facnn 8185  facp1 8188  facnn2 8191  faclbnd3 8199  faclbnd4lem1 8200  faclbnd4lem3 8202  bcpasci 8221  ser1ser0i 8308  ser0mulci 8319  ser1mulci 8320  binomlem2 8327  binomlem3 8328  binomlem6 8331  binomi 8332  clm4i 8340  climaddlem2 8375  climmullem7 8386  climcmplem 8397  caucvglem2 8418  cvgcmpubi 8446  isum1clim 8458  isumshfti 8465  isumshft2i 8466  expcnvlem2 8489  geosumi 8503  cvgratlem2ALT 8510  fsum0diaglem2 8519  elcncf 8527  ivthlem2 8544  ivthlem6 8548  ivthlem7 8549  ivthlem9 8551  efaddlem26 8625  eftlexiOLD 8639  efgt0i 8669  eflti 8671  efcnlem2 8685  sin01bndlem2 8734  cos01bndlem2 8736  sin01gt0 8742  cos01gt0 8743  sin02gt0 8744  xpnnen 8768  ruclem33 8811  ruclem35 8813  infxpidmlem4 8824  infxpidmlem7 8827  infxpidmlem12 8832  infmap2lem1 8848  infmap2 8850  alephadd 8851  alephmul 8852  alephexp1 8853  alephsuc3 8854  alephexp2 8855  subbas 8914  subbas2 8915  sn0top 8917  distop 8919  ntrss2 8966  qdensere 9027  cnpco 9046  msflem 9080  lpbl 9157  tgioo 9193  dscmet 9196  lmle 9238  metelcls 9243  metcnp4 9248  fsumcnlem 9267  iscms2 9272  bcthlem4 9280  bcthlem14 9290  bcthlem22 9298  grpsn 9340  ablmul 9439  ssga 9455  gapmlem 9461  ringi 9466  ringsn 9490  drngi 9493  vci 9499  nvi 9565  nvoprne 9638  vacnlem2 9668  ipfval 9691  nmobndseqi 9780  phpar2 9823  ipasslem5 9835  ubthlem6 9877  minveclem10 9899  minveclem14 9903  spwmo 9999  laspwcl 10011  lanfwcl 10012  pilem2 10021  sincosq1sgn 10053  sincosq2sgn 10054  sincosq3sgn 10055  sincosq4sgn 10056  sinq12gt0t 10057  cosh111lem1 10068  efifolem5 10080  circgrp 10094  shftefif1olem 10095  effoi 10099  axgroth6 10137  twpar2 10149  xp1st 10155  xp2nd 10156  islfin 10168  indexfi 10174  findcard 10178  findcardOLD 10179  symggrpi 10205  stoig2 10252  fbssint 10279  infi 10280  extbas1 10291  cncomp 10331  usinuniop 10341  ismgm 10367  isexid2 10372  smgrpismgm 10379  smgrpisass 10380  mndissmgrp 10386  mndisexid 10387  ring1cl 10415  uznzr 10416  zrdivrng 10418  hvsubeq0i 10562  hvmulcan 10571  hvmulcanOLD 10572  hvmulcan2 10573  bcsiALT 10679  chsscmi 10745  chcmhi 10746  hsn0elch 10753  hhssnv 10767  projlem8 10826  projlem13 10831  shintcli 10926  spanval 10932  dfchj2 10957  sshjcl 10960  shsidmi 10990  spanuni 11100  h1de2i 11109  spansni 11113  spanunsni 11135  cmbr3i 11176  osumlem1 11213  osumlem2 11214  osumlem3 11215  osumcor2i 11225  spansncvi 11232  5oalem7 11240  3oalem3 11244  pjss2i 11260  pjssmii 11261  mayete3i 11308  mayete3OLDi 11309  nmop0h 11553  lnopconi 11600  lnfnconi 11627  riesz3i 11632  nmopcoi 11665  pjnmopi 11719  pjorthcoi 11741  pjssdif1i 11747  elpjch 11761  pjin2i 11766  pjclem1 11768  pjclem2 11769  pjclem4a 11771  pj3lem1 11779  strlem1 11822  strlem3 11825  strlem4 11826  strlem5 11827  stri 11829  hstrlem3 11833  hstrlem4 11834  hstrlem5 11835  hstri 11837  stcltr1i 11846  dmdbr5 11880  mdsl1i 11893  mdslmd1lem2 11898  atn0 11917  atom1d 11925  shatomici 11930  chrelat2i 11937  atssma 11950  irredi 11966  cmmdi 11988  sumdmdi 11992  dmdbr4ati 11993  dmdbr5ati 11994  dmdbr6ati 11995  dmdbr7ati 11996  cdj3lem1 12006  bnj24 12388  bnj44 12419  bnj48OLD 12423  bnj55 12430  bnj143 12475  bnj158 12483  bnj180 12497  bnj214 12508  bnj228 12517  bnj228OLD 12518  bnj512 12519  bnj521 12522  bnj563 12541  bnj566 12544  bnj832 12706  bnj833 12707  bnj834 12708  bnj835 12709  bnj836 12710  bnj837 12711  bnj838 12712  bnj839 12713  bnj840 12714  bnj841 12715  bnj842 12716  bnj843 12717  bnj844 12718  bnj845 12719  bnj846 12720  bnj847 12721  bnj848 12722  bnj769 12723  bnj770 12724  bnj771 12725  bnj772 12726  bnj773 12727  bnj774 12728  bnj775 12729  bnj776 12730  bnj777 12731  bnj778 12732  bnj779 12733  bnj780 12734  bnj781 12735  bnj782 12736  bnj783 12737  bnj784 12738  bnj785 12739  bnj786 12740  bnj787 12741  bnj788 12742  bnj789 12743  bnj790 12744  bnj791 12745  bnj792 12746  bnj793 12747  bnj794 12748  bnj795 12749  bnj796 12750  bnj797 12751  bnj798 12752  bnj799 12753  bnj800 12754  bnj801 12755  bnj802 12756  bnj803 12757  bnj804 12758  bnj805 12759  bnj806 12760  bnj807 12761  bnj808 12762  bnj809 12763  bnj810 12764  bnj811 12765  bnj812 12766  bnj813 12767  bnj814 12768  bnj815 12769  bnj816 12770  bnj817 12771  bnj818 12772  bnj819 12773  bnj820 12774  bnj821 12775  bnj822 12776  bnj823 12777  bnj824 12778  bnj825 12779  bnj826 12780  bnj827 12781  bnj828 12782  bnj829 12783  bnj830 12784  bnj831 12785  bnj862 12795  bnj903 12819  bnj923 12830  bnj922 12834  bnj952 12849  bnj1063 12899  bnj1098 12917  bnj1119 12929  bnj1139 12937  bnj1144 12941  bnj1232 13003  bnj1236 13006  bnj1238 13008  bnj1385 13102  bnj1533 13182  bnj518 13260  bnj522 13261  bnj535 13265  bnj543 13269  bnj544 13270  bnj546 13272  bnj569 13287  bnj590 13298  bnj594 13300  bnj864 13315  bnj849 13318  bnj902 13326  bnj916 13332  bnj944 13340  bnj953 13343  bnj998 13363  bnj1004 13369  bnj1017 13377  bnj1073 13403  bnj1118 13420  bnj1128 13428  bnj1145 13431  bnj1498 13562  seq1resval 13617  fseq1cl 13619  ghomgrpilem2 13629  divalglem1 13697  divalglem6 13701  ndvdsadd 13711  gcdaddmlem 13734  algcvgblem 13745  algfx 13748  eucalginv 13752  eucalglt 13753  eucalg 13755  3prm 13780  untangtr 13802  ressn0 13829  setinds 13844  setinds2f 13845  dfon2lem3 13851  dfon2lem6 13854  dfon2lem7 13855  dfon2lem8 13856  ordsucuniel 13863  predel 13894  frsucopabn 13911  tfisg 13912  tz6.26 13913  wfisg 13917  frmin 13938  frinsg 13941  poxp 13949  frxp 13951  soseq 13955  wfrlem2 13958  wfrlem3 13959  wfrlem4 13960  wfrlem9 13965  wfrlem11 13967  wfrlem12 13968  nofun 13993  nodmon 13994  norn 13995  sltval2 13997  noreson 14001  sltsgn1 14002  sltsgn2 14003  sltintdifex 14004  axbday 14012  axdenselem2 14020  axfelem12 14042  axfelem15 14045  axfelem16 14046  txpss3v 14065  altopth1sn 14090  altopelaltxp 14099  altxpsspw 14100  waj-ax 14238  amosym1 14250  condisd 14270  r19.3rzvb 14273  fampany 14288  nopsthph 14320  evpexun 14322  dfoprab4spop 14339  uninqs 14340  infi1 14343  ficli 14353  domrngref 14364  ref4w 14370  unfinsef 14375  f1fi 14377  fldsqcp2 14378  cpref 14379  inttr 14384  isunscov 14386  restidsing 14391  imrescl 14393  twsymr 14394  prj1 14395  imfstnrelc 14396  prj1b 14397  fixpb 14417  inttrp 14437  onsubcum 14442  celsor 14443  resrelfld 14448  cnveq2 14455  reltrncnv 14457  eqfnung2 14459  surjsec2 14467  inpreima2 14468  prmapcp2 14497  npincppr 14501  repfuntw 14502  repcpwti 14503  cbcpcp 14504  prjmapcp 14507  cbicplem 14508  prjnpl 14510  unprj 14511  prl 14512  dstr 14516  preotr2 14576  dupre2 14585  dupos1 14586  dupos2 14587  inposet 14620  dutos1 14626  dutos2 14627  supwval 14629  pospos 14635  tostos 14637  toplat 14638  dfdir2 14639  fprod1ib 14686  clfsebs 14707  seqzp2 14716  symgfo 14730  curgrpact 14735  fprodneg 14741  prsubrtr 14763  com2i 14765  fldi 14776  vecval3b 14795  svs2 14829  vri 14834  topindis 14859  mapdiscnlem 14870  nsn 14874  cmphmp 14878  top2ind 14897  top2usne 14898  homindlem3 14900  stoig2b 14906  subtopsin2 14907  qusp 14908  topgele 14910  usptop 14920  fgsb 14921  efilcp 14922  fgsb2 14925  efilcp2 14926  cnfilca 14927  rcfpfillem3 14930  rcfpfillem4 14931  rcfpfillem6 14933  rcfpfil 14934  fbaslim2 14936  limvinlv 14941  conttnf 14944  stfincomp 14959  bwt2 14960  clindistop 14962  topgrpi 14972  invtrgrp 14979  bsi2 14992  altretop 14997  cntrsetlem 14999  mlteqer 15017  lteqtpos 15024  mreal 15029  lvsovso3 15040  algi 15074  dedi 15084  cati 15102  0ded 15104  0cat 15105  dualalg 15131  imonclem 15162  issubcat 15193  besubbeca 15196  taralt 15211  empistar 15219  tarax3e 15228  tartwo 15233  tartrel 15239  tartord 15240  cptarc 15242  intartar 15255  intrtael 15256  tartarmap 15265  eltintpar 15276  inttaror 15277  carinttar 15279  cartarlim 15282  fnctartar 15284  fnctartar2 15285  dfiin2gOLD 15356  finminlem 15367  inficlALT 15372  finsschain 15373  hartoglemOLD 15383  hartogOLD 15384  opncldf1 15402  cldbnd 15410  compsublem 15430  compsub 15431  hscptsscld 15434  compfipin0 15436  alexsublem2 15438  alexsublem3 15439  alexsublem4 15440  dfcon2 15442  reconnlem2 15447  reconnlem4 15449  reconnlem5 15450  reconn 15451  2ndc1stc 15477  2ndcctbss 15478  locfincomp 15514  comppfsc 15517  neibastop1 15518  neibastop2lem3 15521  neibastop2 15523  topmtcl 15525  fbasfip 15556  supfil 15560  ufprim 15569  filssufillem 15570  ufinffr 15578  filcon 15580  fcluscomplem 15620  filnetlem1 15640  filnetlem4 15643  prfOLD 15680  inpreima 15682  unpreima 15683  respreima 15684  cocanfo 15689  difxp 15690  upixp 15729  findcard2 15745  fimax 15746  indexfiOLD 15755  inficl 15757  zornn0 15764  frminex 15773  fzsplit 15792  sdclem1 15809  sdclem2 15810  sdc 15811  fdc 15812  seq1eq2 15817  neificl 15841  mettrifi 15847  geomcau 15849  iimulcl 15874  oprpiece1res2 15881  piececn 15894  lmtlm 15908  txmet 15925  sstotbnd 15936  heiborlem10 15964  heiborlem11 15965  heiborlem13 15967  heiborlem21 15975  heiborlem29 15983  heiborlem31 15985  heiborlem33 15987  heiborlem37 15991  heiborlem41 15995  rrnmet 16016  rrncms 16019  rrntotbnd 16022  ismrer1 16024  exidcl 16029  phtpycolem2 16052  phtpycolem3 16053  pcoval2 16075  pcohtpylem2 16081  pcohtpylem3 16082  pcopt 16084  pcoass 16085  flddivrng 16113  riscer 16142  divrngidl 16176  smprngpr 16200  prtlem9 16264  prtlem16 16272  prtlem14 16277  hgralem 16292  pm10.251 16306  pm11.63 16352  ax10ext 16364  ax10-16 16365  pm13.183 16373  iotain 16381  iotasbc 16383  euunianOLD 16396  ipo0 16426  ifr0 16427  trint0 16439  smodm 16445  smofvon 16450  smoel 16451  stb2xpl 16742  stb3xpl 16743  opposet 16912  op0cl 16914  op1cl 16915  hllem1 17020  hlsuprexch 17033  hlhght4 17037  divrngidlemNEW 17165  linepsub 17232  pmapsub 17250  paddasslem9 17289  paddasslem10 17290

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 164

Copyright terms: Public domain