Theorem sylbi 197

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

Hypotheses

Ref	Expression
sylbi.1	⊢ (φ ↔ ψ)
sylbi.2	⊢ (ψ → χ)

Assertion

Ref	Expression
sylbi	⊢ (φ → χ)

Proof of Theorem sylbi

Step	Hyp	Ref	Expression
1		sylbi.1	. . 3 ⊢ (φ ↔ ψ)
2	1	biimpi 149	. 2 ⊢ (φ → ψ)
3		sylbi.2	. 2 ⊢ (ψ → χ)
4	2, 3	syl 10	1 ⊢ (φ → χ)

Syntax hints:   → wi 3   ↔ wb 144

This theorem is referenced by:  3imtr4i 217  pm3.26 317  pm3.27 321  ancoms 438  an1s 489  an1rs 492  an4s 511  pm2.85 582  ordi 599  pm5.18 663  ccase 760  dn1 779  3simpb 792  3simpc 793  3imp 833  3com13 844  syl3anb 875  a6e 1026  19.33b 1128  exintrbi 1154  equvini 1205  sb6x 1225  equs5e 1235  sbf3t 1285  hbsb4t 1287  a12stdy2 1412  a12lem2 1416  euex 1433  eumo0 1434  mooran2 1465  mopick 1472  euor2 1477  2euex 1481  2mo 1487  2eu3 1491  exists2 1499  eqcoms 1521  necon3ai 1649  necon1ai 1651  rexex 1739  ra4 1740  r19.20 1748  r19.22 1777  r19.23ai 1788  r19.36av 1806  r19.37av 1807  r19.44av 1812  r19.45av 1813  elisset 1863  gencl 1874  vtoclgf 1892  cla4gf 1906  rcla4 1917  mo2icl 1969  moi2 1970  moi 1971  reu6 1978  2reuswap 1983  ra4sbc 2047  ra5 2050  csbhypf 2080  sstr2 2123  pssn2lp 2199  ssnpss 2201  unineq 2307  reuun2 2330  disjssun 2379  pssnel 2384  difin0ss 2385  r19.2z 2401  r19.3rzv 2402  ralidm 2411  ifbi 2425  prprc1 2515  pwpw0 2533  sspr 2540  snsssn 2543  preqr2 2547  preq12b 2548  opthpr 2550  opprc1 2563  pwsnALT 2566  reucl 2584  intmin4 2626  iunconst 2640  ssiun 2660  iununi 2686  trss 2763  axrep5 2772  zfrep4 2775  ssex 2793  intex 2803  intnex 2804  intabs 2807  snex 2826  rext 2834  unipw 2836  moabex 2844  nnullss 2846  exss 2847  axpr 2854  opth 2863  copsexg 2868  opprc3 2873  ssopab2 2900  pwssun 2905  solin 2936  frc 2950  frirr 2954  fr2nr 2955  onfr 3014  nlim0 3031  limord 3032  limuni 3033  elsuci 3039  sucprc 3048  ordssun 3069  ordequn 3070  onun2i 3085  euuni 3105  reuunisn 3118  reuxfr 3127  reuunixfr 3129  elpwunsn 3135  fr3nr 3138  onmindif2 3169  suceloni 3170  ordpwsuc 3172  onsucmin 3177  ordsucelsuc 3178  ordsucun 3180  unon 3185  ordunisuc 3186  0elsuc 3189  onuninsuci 3194  nlimsucg 3196  orduninsuc 3197  limsuc 3203  limuni3 3206  tfi 3207  tfis 3208  tfindsg 3213  limomss 3224  limom 3233  findsg 3245  opelxp1 3288  brrelex 3290  ralxp 3301  ralxpf 3303  elvvuni 3315  optocl 3321  0nelelxp 3327  onxpdisj 3328  ssrel 3334  xpsspw 3346  relop 3365  opelxpex2 3369  breldm 3406  elreldm 3425  dmrnssfld 3444  dmcoss 3450  resabs1 3478  relimasn 3517  cnvsym 3529  xpnz 3551  xp11 3561  dmsnop 3577  dfco2a 3599  cores2 3611  coi2 3615  unixp0 3623  relcnvexb 3626  funsn 3648  funopg 3652  imadif 3679  f1ocnvb 3810  ffoss 3822  f1o00 3825  fo00 3826  fvprc 3832  tz6.12-1 3847  ssimaex 3879  fvimacnv 3919  dffo4 3934  exfo 3936  fopabssxp 3938  rnssopab 3939  fopabsn 3954  fopabap 3955  fconst5 3962  abrexexlem1 3972  elunirnALT 3983  f1oweALT 4020  oprssdm 4103  ndmoprcom 4108  1stval2 4150  2ndval2 4151  fo1stres 4156  fo2ndres 4157  1st2val 4158  2nd2val 4159  unielxp 4167  dfoprab5sf 4178  eloprabi 4180  canth 4205  tfrlem4 4215  tfrlem5 4216  tfrlem7 4218  tfrlem8 4219  tfrlem9 4220  rdgsucopabn 4248  frsuc 4254  tz7.48lem 4256  tz7.48-1 4257  abianfplem 4262  abianfp 4263  oaord 4317  nnacom 4373  nnmsucr 4380  nneob 4395  erref 4415  erthi 4421  ereldm 4425  erdisj 4426  ecelqsdm 4440  ectocl 4443  ecoptocl 4444  brecop2 4448  ecopoprdm 4450  th3qlem1 4455  mapprc 4467  mapsspm 4480  map0b 4484  map0 4485  ixpf 4497  uniixp 4498  idssen 4547  ener 4551  en0 4564  en1 4567  2dom 4568  snfi 4573  xpsnen 4576  xpdom2 4583  xpdom3 4586  pw2en 4587  ac6sfi 4591  sbthlem1 4592  sbthlem10 4601  domnsym 4608  domsdomtr 4621  pwuninel 4631  2pwuninel 4632  mapdom1 4639  mapdom2lem 4640  mapdom2 4641  mapxpen 4642  mapunen 4649  ssenen 4651  php 4660  php3 4662  0sdom1dom 4671  ominf 4675  isfinite1 4677  pssnn 4681  ssfi 4683  infcntss 4699  unifi 4701  fiint 4703  abfii4 4707  fodomfi 4709  pwfi 4714  sucprcreg 4743  inf0 4751  inf3lem1 4758  infeq5 4766  dfom3 4776  trcl 4791  zfregs 4793  setind2 4795  r1tr 4800  r1val1 4804  tz9.12lem1 4805  tz9.12lem3 4807  rankr1 4820  rankel 4826  ranklim 4831  rankuni2 4836  rankun 4837  rankeq0 4842  rankr1id 4843  rankuni 4844  rankxpsuc 4861  scottex 4862  scott0 4863  bnd2 4870  karden 4872  hta 4874  aceq4 4880  aceq5lem4 4884  aceq5 4886  aceq6b 4888  ac7 4894  ac6lem 4900  ac6sf 4906  ac6s4 4907  kmlem2 4912  kmlem4 4914  kmlem12 4922  kmlem13 4923  weth 4933  zorn2lem6 4939  zorn2lem7 4940  zorn 4943  brdom5 4948  brdom4 4949  unidom 4954  sucdom 4992  unxpdomlem 4993  carduni 5008  cardiun 5009  alephfp 5050  alephval2 5052  cardcf 5061  cfeq0 5064  cfsuc 5065  nnaun 5091  indpi 5188  prn0 5247  prpssnq 5248  1pr 5271  distrlem3pr 5283  prlem934b 5292  ltexprlem4 5299  reclem2pr 5311  mulcmpblnr 5337  recexsrlem 5366  map2psrpr 5374  suppsr3 5378  supsrlem2 5380  pre-axsup 5445  1re 5589  0re 5594  xrltnr 5695  addgegt0i 5754  msqgt0i 5767  redivcli 5938  prodgt0i 5959  ltdiv2 6032  sup3 6220  xrsupsslem 6244  xrinfmsslem 6245  xrsupss 6246  xrinfmss 6247  elnnz1 6323  znegcl 6331  elnn0nn 6339  zeo 6370  nn0ind 6383  nn0ind-raph 6385  qre 6398  qnegcl 6409  qreccl 6412  eluzelz 6550  eluzel2 6551  eluzle 6552  eluzaddi 6563  eluzsubi 6564  uzind4i 6581  elfzel2i 6607  eluzfz1 6615  om2uzrani 6663  uzrdgvali 6666  cardfz 6671  seq1lem1 6674  seq1suclem 6681  seqzp1 6743  exple1 6804  discrlem3 6859  discrlem 6860  nnesqi 6863  sqrlem6 6879  sqrlem16 6889  sqrthi 6900  sqrcli 6901  sqrge0i 6903  crui 6938  crreczi 6942  negrebi 6996  recvalzi 7090  cjdivi 7091  cau3iri 7118  cau4ii 7121  cau5i 7122  cvg1i 7123  cvg1 7124  facnn 7136  facp1 7139  facnn2 7142  faclbnd3 7150  faclbnd4lem1 7151  faclbnd4lem3 7153  bcpasci 7172  ser1ser0i 7251  ser0mulci 7262  ser1mulci 7263  binomlem2 7270  binomlem3 7271  binomlem6 7274  binomi 7275  clm4i 7283  climaddlem2 7318  climmullem7 7329  climcmplem 7340  caucvglem2 7361  cvgcmpubi 7389  isum1clim 7401  isumshfti 7408  isumshft2i 7409  expcnvlem2 7432  geosumi 7446  cvgratlem2ALT 7453  fsum0diaglem2 7462  elcncf 7470  ivthlem2 7487  ivthlem6 7491  ivthlem7 7492  ivthlem9 7494  efaddlem26 7568  eftlexiOLD 7582  efgt0i 7612  eflti 7614  efcnlem2 7628  sin01bndlem2 7677  cos01bndlem2 7679  sin01gt0 7685  cos01gt0 7686  sin02gt0 7687  xpnnen 7711  ruclem33 7754  ruclem35 7756  infxpidmlem4 7767  infxpidmlem7 7770  infxpidmlem12 7775  infmap2lem1 7791  infmap2 7793  alephadd 7794  alephmul 7795  alephexp1 7796  alephsuc3 7797  alephexp2 7798  subbas 7856  subbas2 7857  sn0top 7859  distop 7861  ntrss2 7900  qdensere 7961  cnpco 7979  msflem 8013  lpbl 8090  tgioo 8126  dscmet 8129  lmle 8171  metelcls 8176  metcnp4 8181  fsumcnlem 8200  iscms2 8205  bcthlem4 8213  bcthlem14 8223  bcthlem22 8231  grpsn 8273  ablmul 8372  ringi 8383  ringsn 8405  drngi 8408  vci 8414  nvi 8480  nvoprne 8553  vacnlem2 8583  ipfval 8606  nmobndseqi 8695  phpar2 8738  ipasslem5 8750  ubthlem6 8792  minveclem10 8814  minveclem14 8818  spwmo 8918  laspwcl 8930  lanfwcl 8931  pilem2 8939  sincosq1sgn 8971  sincosq2sgn 8972  sincosq3sgn 8973  sincosq4sgn 8974  sinq12gt0t 8975  cosh111lem1 8986  efifolem5 8998  circgrp 9012  shftefif1olem 9013  effoi 9017  hvsubeq0i 9205  hvmulcan 9214  hvmulcanOLD 9215  hvmulcan2 9216  bcsiALT 9322  chsscmi 9388  chcmhi 9389  hsn0elch 9396  hhssnv 9410  projlem8 9469  projlem13 9474  shintcli 9569  spanval 9575  dfchj2 9600  sshjcl 9603  shsidmi 9633  spanuni 9743  h1de2i 9752  spansni 9756  spanunsni 9778  cmbr3i 9819  osumlem1 9856  osumlem2 9857  osumlem3 9858  osumcor2i 9868  spansncvi 9875  5oalem7 9883  3oalem3 9887  pjss2i 9903  pjssmii 9904  mayete3i 9951  mayete3OLDi 9952  nmop0h 10195  lnopconi 10242  lnfnconi 10269  riesz3i 10274  nmopcoi 10307  pjnmopi 10355  pjorthcoi 10377  pjssdif1i 10383  elpjch 10397  pjin2i 10402  pjclem1 10404  pjclem2 10405  pjclem4a 10407  pj3lem1 10415  hstcl 10425  hst1a 10426  hstel2 10427  strlem1 10458  strlem3 10461  strlem4 10462  strlem5 10463  stri 10465  hstrlem3 10469  hstrlem4 10470  hstrlem5 10471  hstri 10473  stcltr1i 10482  dmdbr5 10516  mdsl1i 10529  mdslmd1lem2 10534  atn0 10553  atom1d 10561  shatomici 10566  chrelat2i 10573  atssma 10587  irredi 10603  cmmdi 10625  sumdmdi 10629  dmdbr4ati 10630  dmdbr5ati 10631  dmdbr6ati 10632  dmdbr7ati 10633  cdj3lem1 10643  ghomgrpilem2 10671  symggrpi 10691  r19.3rzvb 10721  uninqs 10730  infi1 10735  ficli 10756  domrngref 10764  domintref 10767  ref3w 10772  twpar2 10773  unfinsef 10775  f1fi 10779  fldsqcp2 10780  fldsqcp 10781  cpref 10782  inttr 10787  mlteqer 10789  isunscov 10796  islfin 10799  restidsing 10805  imrescl 10807  twsymr 10808  prj1 10809  imfstnrelc 10810  prj1b 10811  infi 10854  inposet 10868  dupos1 10876  dupos2 10879  lteqtpos 10880  pospos 10882  tostos 10883  toplat 10884  ismgm 10897  isexid2 10901  smgrpismgm 10909  smgrpisass 10910  seqzp2 10918  mndissmgrp 10921  mndisexid 10922  com2i 10941  ring1cl 10966  uznzr 10967  zrdivrng 10969  fldi 10974  vri 10981  topindis 11009  mapdiscn 11014  nsn 11017  cmphmp 11027  top2ind 11050  top2usne 11051  homindlem3 11053  stoig2 11065  subtopsin2 11067  qusp 11068  fgsb 11082  efilcp 11083  fgsb2 11086  efilcp2 11087  cnfilca 11088  rcfpfillem3 11091  rcfpfillem4 11092  rcfpfillem6 11094  rcfpfil 11095  stfincomp 11122  bwt2 11123  usinuniop 11128  clindistop 11131  bsi2 11139  altretop 11144  algi 11181  dedi 11191  cati 11209  0ded 11211  0cat 11212  imonclem 11268  issubcat 11299  besubbeca 11302  dfiin2g 11400  finminlem 11418  inficlALT 11424  finsschain 11425  hartoglem 11435  hartog 11436  opncldf1 11454  cldbnd 11462  compsublem 11487  compsub 11488  hscptsscld 11491  compfipin0 11493  cncomp 11494  alexsublem2 11497  alexsublem3 11498  alexsublem4 11499  dfcon2 11501  reconnlem2 11508  reconnlem4 11510  reconnlem5 11511  reconn 11512  2ndc1stc 11538  2ndcctbss 11539  locfincomp 11575  comppfsc 11578  neibastop1 11579  neibastop2lem3 11582  neibastop2 11584  topmtcl 11586  fbssint 11626  fbasfip 11627  extbas1 11641  supfil 11645  ufprim 11654  filssufillem 11655  ufinffr 11663  filcon 11665  fcluscomplem 11732  filnetlem1 11763  filnetlem4 11766  ssga 11777  gapmlem 11783  inpreima 11793  unpreima 11794  respreima 11795  xp1st 11796  xp2nd 11797  difxp 11798  upixp 11823  findcard 11836  fimax 11837  indexf 11847  inficl 11849  sdclem1 11875  sdclem2 11876  sdc 11877  neificl 11904  mettrifi 11912  geomcau 11914  iimulcl 11938  piececn 11955  lmtlm 11969  sstotbnd 11992  heiborlem10 12020  heiborlem11 12021  heiborlem13 12023  heiborlem21 12031  heiborlem29 12039  heiborlem31 12041  heiborlem33 12043  heiborlem37 12047  heiborlem41 12051  rrnmet 12072  rrncms 12075  rrntotbnd 12078  ismrer1 12080  phtpyid 12091  phtpycolem2 12094  phtpycolem3 12095  hgralem 12196

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 145

Copyright terms: Public domain