MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  sylbir Structured version   Unicode version

Theorem sylbir 206
Description: A mixed syllogism inference from a biconditional and an implication. (Contributed by NM, 5-Aug-1993.)
Hypotheses
Ref Expression
sylbir.1  |-  ( ps  <->  ph )
sylbir.2  |-  ( ps 
->  ch )
Assertion
Ref Expression
sylbir  |-  ( ph  ->  ch )

Proof of Theorem sylbir
StepHypRef Expression
1 sylbir.1 . . 3  |-  ( ps  <->  ph )
21biimpri 199 . 2  |-  ( ph  ->  ps )
3 sylbir.2 . 2  |-  ( ps 
->  ch )
42, 3syl 16 1  |-  ( ph  ->  ch )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 178
This theorem is referenced by:  3imtr3i  258  ex  425  3ori  1245  19.38  1813  equsex  2003  ax12olem3  2008  ax12olem5OLD  2016  sbi2  2135  sb5rf  2168  ax11eq  2272  ax11el  2273  mo  2305  mo2  2312  2mo  2361  axie2  2414  bm1.1  2423  necon1i  2650  sbhypf  3003  vtocl2  3009  vtocl3  3010  reu6  3125  uneqin  3594  inelcm  3684  difin0ss  3696  difprsn1  3937  tppreqb  3941  unissint  4076  intminss  4078  iununi  4177  bm1.3ii  4335  moabex  4424  copsex2g  4446  opelopabt  4469  eusv2nf  4723  reusv3i  4732  reuxfr2d  4748  onminesb  4780  onminsb  4781  onintrab  4783  onnminsb  4786  onsucuni2  4816  tfindsg2  4843  eqrelrel  4979  opeliunxp2  5015  opelrn  5103  issref  5249  ssxpb  5305  xpima  5315  dmsn0el  5341  relcoi2  5399  iotanul  5435  dffv2  5798  fnfvrnss  5898  fressnfv  5922  fconst5  5951  fconstfv  5956  zfrep6  5970  f1mpt  6009  isocnv3  6054  f1owe  6075  ovprc  6110  fo1stres  6372  fo2ndres  6373  bropopvvv  6428  frxp  6458  mpt2xopoveqd  6474  reldmtpos  6489  tfrlem5  6643  tfrlem9  6648  tfr2  6661  rdgsuc  6684  oaordi  6791  oeordi  6832  omopthi  6902  fvmptmap  7052  mptelixpg  7101  ener  7156  domtr  7162  snfi  7189  unen  7191  xpf1o  7271  mapen  7273  unxpdomlem3  7317  isinf  7324  frfi  7354  unblem1  7361  unfi  7376  fofinf1o  7389  inf3lem2  7586  inf3lem5  7589  cantnfreslem  7633  cantnfp1lem1  7636  cantnfp1lem3  7638  tcmin  7682  r1ordg  7706  r1ord  7708  rankr1ai  7726  r1val3  7766  bndrank  7769  unbndrank  7770  rankr1b  7792  rankxplim3  7807  tcrank  7810  xpnum  7840  cardmin2  7887  infxpenlem  7897  fseqen  7910  dfac8clem  7915  alephsson  7983  alephfp  7991  dfac4  8005  kmlem6  8037  kmlem8  8039  kmlem9  8040  infpssr  8190  fin1a2lem12  8293  axcc4  8321  axcc4dom  8323  ac6s2  8368  zornn0g  8387  cardidg  8425  unsnen  8430  pwcfsdom  8460  cfpwsdom  8461  gchpwdom  8551  r1tskina  8659  intgru  8691  indpi  8786  nqereu  8808  supsrlem  8988  letrii  9200  infmrcl  9989  dfnn3  10016  zaddcl  10319  uzindOLD  10366  nn0ind  10368  fnn0ind  10371  ublbneg  10562  fzo0end  11190  elfznelfzo  11194  fzind2  11200  injresinjlem  11201  faclbnd4lem1  11586  hashinf  11625  hasheqf1oi  11637  hashgt0elex  11672  hash2prde  11690  hashfacen  11705  rediv  11938  imdiv  11945  sqr0  12049  fsump1i  12555  cos1bnd  12790  sinltx  12792  rpnnen2lem1  12816  rpnnen2lem2  12817  rpnnen2  12827  odd2np1  12910  gcdcllem1  13013  gcdaddmlem  13030  algfx  13073  odzval  13179  odzdvds  13183  opoe  13187  omoe  13188  opeo  13189  omeo  13190  prmreclem5  13290  mul4sq  13324  imasaddfnlem  13755  mreexexlem4d  13874  lubval  14438  glbval  14443  joinlem  14449  meetlem  14456  clatlem  14541  gictr  15064  cntzval  15122  efgsfo  15373  efgrelexlemb  15384  dprd2da  15602  lssacs  16045  cnfldinv  16734  ocvval  16896  eltopspOLD  16985  tpsexOLD  16986  opnnei  17186  ordtbas2  17257  ordtrest2lem  17269  lmmo  17446  fincmp  17458  txbas  17601  ptcnplem  17655  tx2ndc  17685  hmphtr  17817  fbun  17874  filcon  17917  ptcmplem5  18089  cnextcn  18100  utoptop  18266  restutopopn  18270  ucncn  18317  metustOLD  18599  metust  18600  cfilucfilOLD  18601  cfilucfil  18602  elcncf1di  18927  xrhmeo  18973  phtpycc  19018  copco  19045  pcohtpylem  19046  pcopt  19049  pcopt2  19050  ovolval  19372  iunmbl2  19453  itg2splitlem  19642  cpnfval  19820  plyval  20114  fta1  20227  aaliou2b  20260  ulmdvlem3  20320  radcnvlem2  20332  dvradcnv  20339  reeff1o  20365  sincosq1lem  20407  sincosq2sgn  20409  sincosq4sgn  20411  sinq12ge0  20418  logrncl  20467  eflog  20476  cxpge0  20576  atanf  20722  atanbnd  20768  lgsne0  21119  mul2sq  21151  pntibnd  21289  ostth  21335  isusgra0  21378  usgraedg4  21408  nbusgra  21442  nbgranself2  21450  wlkntrllem3  21563  spthonepeq  21589  wlkdvspth  21610  cyclnspth  21620  3v3e3cycl2  21653  3v3e3cycl  21654  4cycl4dv  21656  vdgrf  21671  eupath2lem1  21701  isgrpo  21786  ismgm  21910  isrngo  21968  rngoablo2  22012  rngoueqz  22020  isdivrngo  22021  vci  22029  vcex  22061  nmogtmnf  22273  siilem1  22354  siii  22356  ajmoi  22362  bcsiALT  22683  hhcms  22707  ocval  22784  hsupval  22838  omlsilem  22906  h1de2bi  23058  h1de2ctlem  23059  hosubeq0i  23331  adjmo  23337  nmopgtmnf  23373  nlfnval  23386  nmcopex  23534  nmcfnex  23558  riesz4i  23568  riesz1  23570  riesz2  23571  opsqrlem1  23645  superpos  23859  hatomistici  23867  chpssati  23868  mdsymlem3  23910  mdsymi  23916  3o1cs  23955  3o2cs  23956  3o3cs  23957  qqhval2  24368  logb1  24405  esumfsup  24462  esumcvg  24478  cntnevol  24584  dya2icoseg2  24630  dya2iocnei  24634  cndprobprob  24698  ballotlemsdom  24771  ballotth  24797  igamf  24837  igamcl  24838  txpcon  24921  ghomgrp  25103  setinds  25407  dfon2lem7  25418  dfon2lem8  25419  nnsinds  25494  nn0sinds  25495  poseq  25530  soseq  25531  wfrlem4  25543  wfrlem12  25551  wfrlem16  25555  wfr2  25557  frrlem4  25587  frrlem11  25596  nodenselem4  25641  nocvxminlem  25647  nocvxmin  25648  pprodss4v  25731  fullfunfv  25794  altxpsspw  25824  mptelee  25836  axlowdimlem9  25891  axlowdimlem12  25894  axcontlem2  25906  axcontlem12  25916  funtransport  25967  fvtransport  25968  funray  26076  fvray  26077  funline  26078  fvline  26080  bpolydiflem  26102  bpoly3  26106  bpoly4  26107  bisym1  26171  onsucconi  26189  onsucsuccmpi  26195  ismblfin  26249  itg2addnclem  26258  finminlem  26323  sdclem2  26448  totbndbnd  26500  exidresid  26556  isdrngo1  26574  isdrngo2  26576  ispridl2  26650  prtlem11  26717  mptfcl  26779  fphpd  26879  elmnc  27320  itgoval  27345  pm11.71  27575  iotavalsb  27612  sbiota1  27613  stoweidlem3  27730  stoweidlem17  27744  rexrsb  27925  raaan2  27931  afv0nbfvbi  27993  afvfv0bi  27994  afveu  27995  fnbrafvb  27996  afvres  28014  tz6.12-afv  28015  dmfcoafv  28017  afvco2  28018  aovprc  28030  aovrcl  28031  aovmpt4g  28043  fzo1fzo0n0  28130  2ffzoeq  28142  swrdswrdlem  28200  swrdccatin12lem4  28215  swrdccat3  28217  swrdccat3blem  28220  2cshwmod  28259  cshw1  28277  cshwssizelem1a  28281  2wlkeq  28305  usg2wlkeq  28306  2wlkonot3v  28344  2spthonot3v  28345  2spontn0vne  28356  usgfiregdegfi  28363  frgra2v  28391  frgra3vlem1  28392  frgra3vlem2  28393  frgrancvvdeqlem2  28422  frgrancvvdeqlem3  28423  frgrancvvdeqlemB  28429  frgrancvvdeqlemC  28430  frgrawopreglem5  28439  usgreghash2spot  28460  secval  28492  cscval  28493  cotval  28494  2uasbanh  28650  eel0TT  28809  eelT00  28810  eelTTT  28811  eelT11  28813  eelT12  28817  eelTT1  28819  eelT01  28820  eel0T1  28821  eelTT  28885  uunT1p1  28895  uun121  28897  uun121p1  28898  un2122  28904  uunTT1  28907  uunTT1p1  28908  uunTT1p2  28909  uunT11  28910  uunT11p1  28911  uunT11p2  28912  uunT12  28913  uunT12p1  28914  uunT12p2  28915  uunT12p3  28916  uunT12p4  28917  uunT12p5  28918  uun111  28919  3anidm12p2  28921  uun123  28922  3impdirp1  28930  undif3VD  28996  a9e2ndeqVD  29023  2uasbanhVD  29025  a9e2ndeqALT  29045  iunconlem2  29049  sineq0ALT  29051  bnj945  29146  bnj1379  29204  bnj1459  29216  bnj557  29274  bnj571  29279  bnj849  29298  bnj964  29316  bnj978  29322  bnj1018  29335  bnj1020  29336  bnj1033  29340  bnj1175  29375  bnj1398  29405  bnj1417  29412  bnj1523  29442  sbi2NEW7  29566  sb5rfNEW7  29593  lkr0f  29894  hl2at  30204  dalemswapyz  30455  pclfinclN  30749  osumcllem11N  30765  pexmidlem8N  30776  ltrnnid  30935
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 179
  Copyright terms: Public domain W3C validator