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

Theorem sylbir 205
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 198 . 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 177
This theorem is referenced by:  3imtr3i  257  ex  424  3ori  1244  19.38  1808  equsex  1969  ax12olem3  1974  ax12olem5OLD  1981  sbi2  2113  sb5rf  2139  ax11eq  2243  ax11el  2244  mo  2276  mo2  2283  2mo  2332  axie2  2379  bm1.1  2389  necon1i  2611  sbhypf  2961  vtocl2  2967  vtocl3  2968  reu6  3083  uneqin  3552  inelcm  3642  difin0ss  3654  difprsn1  3895  tppreqb  3899  unissint  4034  intminss  4036  iununi  4135  bm1.3ii  4293  moabex  4382  copsex2g  4404  opelopabt  4427  eusv2nf  4680  reusv3i  4689  reuxfr2d  4705  onminesb  4737  onminsb  4738  onintrab  4740  onnminsb  4743  onsucuni2  4773  tfindsg2  4800  eqrelrel  4936  opeliunxp2  4972  opelrn  5060  issref  5206  ssxpb  5262  xpima  5272  dmsn0el  5298  relcoi2  5356  iotanul  5392  dffv2  5755  fnfvrnss  5855  fressnfv  5879  fconst5  5908  fconstfv  5913  zfrep6  5927  f1mpt  5966  isocnv3  6011  f1owe  6032  ovprc  6067  fo1stres  6329  fo2ndres  6330  bropopvvv  6385  frxp  6415  mpt2xopoveqd  6431  reldmtpos  6446  tfrlem5  6600  tfrlem9  6605  tfr2  6618  rdgsuc  6641  oaordi  6748  oeordi  6789  omopthi  6859  fvmptmap  7009  mptelixpg  7058  ener  7113  domtr  7119  snfi  7146  unen  7148  xpf1o  7228  mapen  7230  unxpdomlem3  7274  isinf  7281  frfi  7311  unblem1  7318  unfi  7333  fofinf1o  7346  inf3lem2  7540  inf3lem5  7543  cantnfreslem  7587  cantnfp1lem1  7590  cantnfp1lem3  7592  tcmin  7636  r1ordg  7660  r1ord  7662  rankr1ai  7680  r1val3  7720  bndrank  7723  unbndrank  7724  rankr1b  7746  rankxplim3  7761  tcrank  7764  xpnum  7794  cardmin2  7841  infxpenlem  7851  fseqen  7864  dfac8clem  7869  alephsson  7937  alephfp  7945  dfac4  7959  kmlem6  7991  kmlem8  7993  kmlem9  7994  infpssr  8144  fin1a2lem12  8247  axcc4  8275  axcc4dom  8277  ac6s2  8322  zornn0g  8341  cardidg  8379  unsnen  8384  pwcfsdom  8414  cfpwsdom  8415  gchpwdom  8505  r1tskina  8613  intgru  8645  indpi  8740  nqereu  8762  supsrlem  8942  letrii  9154  infmrcl  9943  dfnn3  9970  zaddcl  10273  uzindOLD  10320  nn0ind  10322  fnn0ind  10325  ublbneg  10516  fzo0end  11143  elfznelfzo  11147  fzind2  11153  injresinjlem  11154  faclbnd4lem1  11539  hashinf  11578  hasheqf1oi  11590  hashgt0elex  11625  hash2prde  11643  hashfacen  11658  rediv  11891  imdiv  11898  sqr0  12002  fsump1i  12508  cos1bnd  12743  sinltx  12745  rpnnen2lem1  12769  rpnnen2lem2  12770  rpnnen2  12780  odd2np1  12863  gcdcllem1  12966  gcdaddmlem  12983  algfx  13026  odzval  13132  odzdvds  13136  opoe  13140  omoe  13141  opeo  13142  omeo  13143  prmreclem5  13243  mul4sq  13277  imasaddfnlem  13708  mreexexlem4d  13827  lubval  14391  glbval  14396  joinlem  14402  meetlem  14409  clatlem  14494  gictr  15017  cntzval  15075  efgsfo  15326  efgrelexlemb  15337  dprd2da  15555  lssacs  15998  cnfldinv  16687  ocvval  16849  eltopspOLD  16938  tpsexOLD  16939  opnnei  17139  ordtbas2  17209  ordtrest2lem  17221  lmmo  17398  fincmp  17410  txbas  17552  ptcnplem  17606  tx2ndc  17636  hmphtr  17768  fbun  17825  filcon  17868  ptcmplem5  18040  cnextcn  18051  utoptop  18217  restutopopn  18221  ucncn  18268  metustOLD  18550  metust  18551  cfilucfilOLD  18552  cfilucfil  18553  elcncf1di  18878  xrhmeo  18924  phtpycc  18969  copco  18996  pcohtpylem  18997  pcopt  19000  pcopt2  19001  ovolval  19323  iunmbl2  19404  itg2splitlem  19593  cpnfval  19771  plyval  20065  fta1  20178  aaliou2b  20211  ulmdvlem3  20271  radcnvlem2  20283  dvradcnv  20290  reeff1o  20316  sincosq1lem  20358  sincosq2sgn  20360  sincosq4sgn  20362  sinq12ge0  20369  logrncl  20418  eflog  20427  cxpge0  20527  atanf  20673  atanbnd  20719  lgsne0  21070  mul2sq  21102  pntibnd  21240  ostth  21286  isusgra0  21329  usgraedg4  21359  nbusgra  21393  nbgranself2  21401  wlkntrllem3  21514  spthonepeq  21540  wlkdvspth  21561  cyclnspth  21571  3v3e3cycl2  21604  3v3e3cycl  21605  4cycl4dv  21607  vdgrf  21622  eupath2lem1  21652  isgrpo  21737  ismgm  21861  isrngo  21919  rngoablo2  21963  rngoueqz  21971  isdivrngo  21972  vci  21980  vcex  22012  nmogtmnf  22224  siilem1  22305  siii  22307  ajmoi  22313  bcsiALT  22634  hhcms  22658  ocval  22735  hsupval  22789  omlsilem  22857  h1de2bi  23009  h1de2ctlem  23010  hosubeq0i  23282  adjmo  23288  nmopgtmnf  23324  nlfnval  23337  nmcopex  23485  nmcfnex  23509  riesz4i  23519  riesz1  23521  riesz2  23522  opsqrlem1  23596  superpos  23810  hatomistici  23818  chpssati  23819  mdsymlem3  23861  mdsymi  23867  3o1cs  23906  3o2cs  23907  3o3cs  23908  qqhval2  24319  logb1  24356  esumfsup  24413  esumcvg  24429  cntnevol  24535  dya2icoseg2  24581  dya2iocnei  24585  cndprobprob  24649  ballotlemsdom  24722  ballotth  24748  igamf  24788  igamcl  24789  txpcon  24872  ghomgrp  25054  setinds  25348  dfon2lem7  25359  dfon2lem8  25360  nnsinds  25431  nn0sinds  25432  poseq  25467  soseq  25468  wfrlem4  25473  wfrlem12  25481  wfrlem16  25485  wfr2  25487  tfrALTlem  25490  frrlem4  25498  frrlem11  25507  nodenselem4  25552  nocvxminlem  25558  nocvxmin  25559  pprodss4v  25638  fullfunfv  25700  altxpsspw  25726  mptelee  25738  axlowdimlem9  25793  axlowdimlem12  25796  axcontlem2  25808  axcontlem12  25818  funtransport  25869  fvtransport  25870  funray  25978  fvray  25979  funline  25980  fvline  25982  bpolydiflem  26004  bpoly3  26008  bpoly4  26009  bisym1  26073  onsucconi  26091  onsucsuccmpi  26097  ismblfin  26146  itg2addnclem  26155  finminlem  26211  sdclem2  26336  totbndbnd  26388  exidresid  26444  isdrngo1  26462  isdrngo2  26464  ispridl2  26538  prtlem11  26605  mptfcl  26667  fphpd  26767  elmnc  27209  itgoval  27234  pm11.71  27464  iotavalsb  27501  sbiota1  27502  stoweidlem3  27619  stoweidlem17  27633  rexrsb  27814  raaan2  27820  afv0nbfvbi  27882  afvfv0bi  27883  afveu  27884  fnbrafvb  27885  afvres  27903  tz6.12-afv  27904  dmfcoafv  27906  afvco2  27907  aovprc  27919  aovrcl  27920  aovmpt4g  27932  fzo1fzo0n0  27988  swrdswrdlem  28010  swrdccatin2  28018  swrdccatin12lem4  28025  swrdccatin12b  28027  swrdccatin12c  28028  swrdccat3b  28031  2wlkonot3v  28072  2spthonot3v  28073  2spontn0vne  28084  usgfiregdegfi  28091  frgra2v  28103  frgra3vlem1  28104  frgra3vlem2  28105  frgrancvvdeqlem2  28134  frgrancvvdeqlem3  28135  frgrancvvdeqlemB  28141  frgrancvvdeqlemC  28142  frgrawopreglem5  28151  usgreghash2spot  28172  secval  28204  cscval  28205  cotval  28206  2uasbanh  28359  eel0TT  28516  eelT00  28517  eelTTT  28518  eelT11  28520  eelT12  28524  eelTT1  28526  eelT01  28527  eel0T1  28528  eelTT  28592  uunT1p1  28602  uun121  28604  uun121p1  28605  un2122  28611  uunTT1  28614  uunTT1p1  28615  uunTT1p2  28616  uunT11  28617  uunT11p1  28618  uunT11p2  28619  uunT12  28620  uunT12p1  28621  uunT12p2  28622  uunT12p3  28623  uunT12p4  28624  uunT12p5  28625  uun111  28626  3anidm12p2  28628  uun123  28629  3impdirp1  28637  undif3VD  28703  a9e2ndeqVD  28730  2uasbanhVD  28732  a9e2ndeqALT  28753  bnj945  28850  bnj1379  28908  bnj1459  28920  bnj557  28978  bnj571  28983  bnj849  29002  bnj964  29020  bnj978  29026  bnj1018  29039  bnj1020  29040  bnj1033  29044  bnj1175  29079  bnj1398  29109  bnj1417  29116  bnj1523  29146  sbi2NEW7  29268  sb5rfNEW7  29292  lkr0f  29577  hl2at  29887  dalemswapyz  30138  pclfinclN  30432  osumcllem11N  30448  pexmidlem8N  30459  ltrnnid  30618
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 178
  Copyright terms: Public domain W3C validator