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

Theorem sylbir 204
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 197 . 2  |-  ( ph  ->  ps )
3 sylbir.2 . 2  |-  ( ps 
->  ch )
42, 3syl 15 1  |-  ( ph  ->  ch )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176
This theorem is referenced by:  3imtr3i  256  ex  423  3ori  1242  ax12olem5  1872  sbi2  2004  sb5rf  2030  ax11eq  2132  ax11el  2133  mo  2165  mo2  2172  2mo  2221  bm1.1  2268  necon1i  2490  sbhypf  2833  vtocl2  2839  vtocl3  2840  reu6  2954  uneqin  3420  inelcm  3509  difin0ss  3520  unissint  3886  intminss  3888  iununi  3986  bm1.3ii  4144  moabex  4232  copsex2g  4254  opelopabt  4277  eusv2nf  4532  reusv3i  4541  reuxfr2d  4557  eldifpw  4566  onminesb  4589  onminsb  4590  onintrab  4592  onnminsb  4595  onsucuni2  4625  tfindsg2  4652  eqrelrel  4788  opeliunxp2  4824  opelrn  4910  issref  5056  ssxpb  5110  dmsn0el  5142  relcoi2  5200  iotanul  5234  dffv2  5592  fnfvrnss  5687  fressnfv  5707  fconst5  5731  fconstfv  5734  zfrep6  5748  f1mpt  5785  isocnv3  5829  f1owe  5850  ovprc  5885  fo1stres  6143  fo2ndres  6144  frxp  6225  reldmtpos  6242  tfrlem5  6396  tfrlem9  6401  tfr2  6414  rdgsuc  6437  oaordi  6544  oeordi  6585  omopthi  6655  fvmptmap  6804  mptelixpg  6853  ener  6908  domtr  6914  snfi  6941  unen  6943  xpf1o  7023  mapen  7025  unxpdomlem3  7069  isinf  7076  frfi  7102  unblem1  7109  unfi  7124  fofinf1o  7137  inf3lem2  7330  inf3lem5  7333  cantnfreslem  7377  cantnfp1lem1  7380  cantnfp1lem3  7382  tcmin  7426  r1ordg  7450  r1ord  7452  rankr1ai  7470  r1val3  7510  bndrank  7513  unbndrank  7514  rankr1b  7536  rankxplim3  7551  tcrank  7554  xpnum  7584  cardmin2  7631  infxpenlem  7641  fseqen  7654  dfac8clem  7659  alephsson  7727  alephfp  7735  dfac4  7749  kmlem6  7781  kmlem8  7783  kmlem9  7784  infpssr  7934  fin1a2lem12  8037  axcc4  8065  axcc4dom  8067  ac6s2  8113  zornn0g  8132  cardidg  8170  unsnen  8175  pwcfsdom  8205  cfpwsdom  8206  gchpwdom  8296  r1tskina  8404  intgru  8436  indpi  8531  nqereu  8553  supsrlem  8733  letrii  8944  infmrcl  9733  dfnn3  9760  zaddcl  10059  uzindOLD  10106  nn0ind  10108  fnn0ind  10111  ublbneg  10302  fzo0end  10915  fzind2  10923  faclbnd4lem1  11306  hashinf  11342  hashfacen  11392  rediv  11616  imdiv  11623  sqr0  11727  fsump1i  12232  cos1bnd  12467  sinltx  12469  rpnnen2lem1  12493  rpnnen2lem2  12494  rpnnen2  12504  odd2np1  12587  gcdcllem1  12690  gcdaddmlem  12707  algfx  12750  odzval  12856  odzdvds  12860  opoe  12864  omoe  12865  opeo  12866  omeo  12867  prmreclem5  12967  mul4sq  13001  imasaddfnlem  13430  mreexexlem4d  13549  lubval  14113  glbval  14118  joinlem  14124  meetlem  14131  clatlem  14216  gictr  14739  cntzval  14797  efgsfo  15048  efgrelexlemb  15059  dprd2da  15277  lssacs  15724  cnfldinv  16405  ocvval  16567  eltopspOLD  16656  tpsexOLD  16657  opnnei  16857  ordtbas2  16921  ordtrest2lem  16933  lmmo  17108  fincmp  17120  txbas  17262  ptcnplem  17315  tx2ndc  17345  hmphtr  17474  fbun  17535  filcon  17578  ptcmplem5  17750  elcncf1di  18399  xrhmeo  18444  phtpycc  18489  copco  18516  pcohtpylem  18517  pcopt  18520  pcopt2  18521  ovolval  18833  iunmbl2  18914  itg2splitlem  19103  cpnfval  19281  plyval  19575  fta1  19688  aaliou2b  19721  ulmdvlem3  19779  radcnvlem2  19790  dvradcnv  19797  reeff1o  19823  sincosq1lem  19865  sincosq2sgn  19867  sincosq4sgn  19869  sinq12ge0  19876  logrncl  19925  eflog  19933  cxpge0  20030  atanf  20176  atanbnd  20222  lgsne0  20572  mul2sq  20604  pntibnd  20742  ostth  20788  isgrpo  20863  ismgm  20987  isrngo  21045  rngoablo2  21089  rngoueqz  21097  isdivrngo  21098  vci  21104  vcex  21136  nmogtmnf  21348  siilem1  21429  siii  21431  ajmoi  21437  bcsiALT  21758  hhcms  21782  ocval  21859  hsupval  21913  omlsilem  21981  h1de2bi  22133  h1de2ctlem  22134  hosubeq0i  22406  adjmo  22412  nmopgtmnf  22448  nlfnval  22461  nmcopex  22609  nmcfnex  22633  riesz4i  22643  riesz1  22645  riesz2  22646  opsqrlem1  22720  superpos  22934  hatomistici  22942  chpssati  22943  mdsymlem3  22985  mdsymi  22991  ballotlemsdom  23070  ballotth  23096  3o1cs  23097  3o2cs  23098  3o3cs  23099  iuninc  23158  cntnevol  23175  xpima  23202  xrsinvgval  23306  logb1  23405  esumcvg  23454  cndprobprob  23641  txpcon  23763  eupath2lem1  23901  ghomgrp  23997  setinds  24134  dfon2lem7  24145  dfon2lem8  24146  nnsinds  24217  nn0sinds  24218  poseq  24253  soseq  24254  wfrlem4  24259  wfrlem12  24267  wfrlem16  24271  wfr2  24273  tfrALTlem  24276  frrlem4  24284  frrlem11  24293  nodenselem4  24338  nocvxminlem  24344  nocvxmin  24345  pprodss4v  24424  fullfunfv  24485  altxpsspw  24511  mptelee  24523  axlowdimlem9  24578  axlowdimlem12  24581  axcontlem2  24593  axcontlem12  24603  funtransport  24654  fvtransport  24655  funray  24763  fvray  24764  funline  24765  fvline  24767  bpolydiflem  24789  bpoly3  24793  bpoly4  24794  bisym1  24858  onsucconi  24876  onsucsuccmpi  24882  alneal1a  25004  boxrim  25007  difeqri2  25040  domintrefb  25063  twsymr  25078  prj1b  25079  prj3  25080  fixpc  25094  celsor  25111  domintrefc  25125  dfps2  25289  svli2  25484  vri  25492  inttop2  25515  limptlimpr2lem2  25575  topunfincomp  25590  hdrmp  25706  algi  25727  tartarmap  25888  inttarcar  25901  pgapspf  26052  pgapspf2  26053  gltpntl  26072  bsstr  26128  nbssntr  26129  lppotoslem  26143  lppotos  26144  nbssntrs  26147  finminlem  26231  sdclem2  26452  totbndbnd  26513  exidresid  26569  isdrngo1  26587  isdrngo2  26589  ispridl2  26663  prtlem11  26734  mptfcl  26798  fphpd  26899  elmnc  27341  itgoval  27366  pm11.71  27596  iotavalsb  27633  sbiota1  27634  stoweidlem3  27752  stoweidlem17  27766  rexrsb  27947  raaan2  27953  afv0nbfvbi  28014  afvfv0bi  28015  fnbrafvb  28016  afvres  28034  tz6.12-afv  28035  dmfcoafv  28036  afvco2  28037  aovprc  28048  aovrcl  28049  aovmpt4g  28061  mpt2xopoveqd  28087  isusgra0  28106  nbgranself2  28151  frgra2v  28177  frgra3vlem1  28178  frgra3vlem2  28179  secval  28217  cscval  28218  cotval  28219  2uasbanh  28327  eel0TT  28479  eelT00  28480  eelTTT  28481  eelT11  28483  eelT12  28486  eelTT1  28488  eelT01  28489  eel0T1  28490  eelTT  28546  uunT1p1  28556  uun121  28558  uun121p1  28559  un2122  28565  uunTT1  28568  uunTT1p1  28569  uunTT1p2  28570  uunT11  28571  uunT11p1  28572  uunT11p2  28573  uunT12  28574  uunT12p1  28575  uunT12p2  28576  uunT12p3  28577  uunT12p4  28578  uunT12p5  28579  uun111  28580  3anidm12p2  28582  uun123  28583  3impdirp1  28591  undif3VD  28658  a9e2ndeqVD  28685  2uasbanhVD  28687  a9e2ndeqALT  28708  bnj945  28805  bnj1379  28863  bnj1459  28875  bnj557  28933  bnj571  28938  bnj849  28957  bnj964  28975  bnj978  28981  bnj1018  28994  bnj1020  28995  bnj1033  28999  bnj1175  29034  bnj1398  29064  bnj1417  29071  bnj1523  29101  a12study5rev  29122  a12study  29132  lkr0f  29284  hl2at  29594  dalemswapyz  29845  pclfinclN  30139  osumcllem11N  30155  pexmidlem8N  30166  ltrnnid  30325
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 177
  Copyright terms: Public domain W3C validator