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

Theorem sylbir 213
Description: A mixed syllogism inference from a biconditional and an implication. (Contributed by NM, 3-Jan-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 206 . 2  |-  ( ph  ->  ps )
3 sylbir.2 . 2  |-  ( ps 
->  ch )
42, 3syl 16 1  |-  ( ph  ->  ch )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem depends on definitions:  df-bi 185
This theorem is referenced by:  3imtr3i  265  ex  434  3ori  1288  19.38  1639  19.35  1664  equsex  2011  nfeqf2  2014  sbi2  2108  sb5rfOLD  2144  ax12eq  2264  ax12el  2265  mo2v  2282  mo2vOLD  2283  mo2vOLDOLD  2284  moOLD  2327  mo2OLD  2336  2mo  2382  2moOLD  2383  2moOLDOLD  2384  axie2  2440  bm1.1OLD  2451  necon1bi  2700  necon1i  2709  sbhypf  3160  vtocl2  3166  vtocl3  3167  reu6  3292  uneqin  3749  inelcm  3881  difin0ss  3893  difprsn1  4163  tppreqb  4168  unissint  4306  intminss  4308  iununi  4410  bm1.3ii  4571  eusv2nf  4645  reusv3i  4654  reuxfr2d  4670  moabex  4706  copsex2g  4735  opelopabt  4759  eqrelrel  5104  opeliunxp2  5141  opelrn  5234  issref  5380  ssxpb  5441  xpima  5449  xpimasn  5452  dmsn0el  5477  relcoi2  5535  iotanul  5566  dffv2  5940  fnfvrnss  6049  fressnfv  6075  fconst5  6118  fconstfv  6123  f1mpt  6157  isocnv3  6216  f1owe  6237  ovprc  6311  onminesb  6617  onminsb  6618  onintrab  6620  onnminsb  6623  onsucuni2  6653  tfindsg2  6680  zfrep6  6752  fo1stres  6808  fo2ndres  6809  bropopvvv  6863  frxp  6893  mpt2xopoveqd  6949  reldmtpos  6963  tfrlem5  7049  tfrlem9  7054  tfr2  7067  rdgsuc  7090  oaordi  7195  oeordi  7236  omopthi  7306  fvmptmap  7455  mptelixpg  7506  ener  7562  domtr  7568  snfi  7596  unen  7598  xpf1o  7679  mapen  7681  unxpdomlem3  7726  isinf  7733  frfi  7765  unblem1  7772  unfi  7787  fofinf1o  7801  fsuppun  7848  inf3lem2  8046  inf3lem5  8049  cantnfp1lem1  8097  cantnfp1lem3  8099  cantnfp1lem1OLD  8123  cantnfp1lem3OLD  8125  tcmin  8172  r1ordg  8196  r1ord  8198  rankr1ai  8216  r1val3  8256  bndrank  8259  unbndrank  8260  rankr1b  8282  rankxplim3  8299  tcrank  8302  xpnum  8332  cardmin2  8379  infxpenlem  8391  fseqen  8408  dfac8clem  8413  alephsson  8481  alephfp  8489  dfac4  8503  kmlem6  8535  kmlem8  8537  kmlem9  8538  infpssr  8688  fin1a2lem12  8791  axcc4  8819  axcc4dom  8821  ac6s2  8866  zornn0g  8885  cardidg  8923  unsnen  8928  pwcfsdom  8958  cfpwsdom  8959  gchpwdom  9048  r1tskina  9160  intgru  9192  indpi  9285  nqereu  9307  supsrlem  9488  letrii  9709  infmrcl  10522  dfnn3  10550  zaddcl  10903  uzindOLD  10955  nn0ind  10957  fnn0ind  10960  ublbneg  11166  nn01to3  11175  fz0  11701  fzo1fzo0n0  11832  elfzom1elp1fzo  11851  fzo0end  11872  elfznelfzo  11883  fzind2  11892  injresinjlem  11893  fleqceilz  11949  fsuppmapnn0fiubex  12066  faclbnd4lem1  12339  hashinf  12378  hasheqf1oi  12392  hashgt0elex  12432  hashfacen  12469  hash2prde  12482  lswcl  12554  lswccats1fst  12602  swrdlsw  12640  swrdswrdlem  12647  swrdccatin12lem3  12678  swrdccat3  12680  swrdccat3blem  12683  cshwsublen  12730  cshwidxmod  12737  repswcshw  12743  cshw1  12753  rediv  12927  imdiv  12934  sqrt0  13038  fsump1i  13547  modfsummods  13570  cos1bnd  13783  sinltx  13785  rpnnen2lem1  13809  rpnnen2lem2  13810  rpnnen2  13820  odd2np1  13905  gcdcllem1  14008  gcdaddmlem  14025  algfx  14068  odzval  14177  odzdvds  14181  opoe  14194  omoe  14195  opeo  14196  omeo  14197  prmreclem5  14297  mul4sq  14331  imasaddfnlem  14783  mreexexlem4d  14902  joindmss  15494  meetdmss  15508  gictr  16128  cntzval  16164  symg2bas  16228  efgsfo  16563  efgrelexlemb  16574  dprddomcld  16835  dprdsubg  16873  dprd2da  16893  lssacs  17413  cnfldinv  18248  ocvval  18493  dmatmul  18794  mdetfval1  18887  mndifsplit  18933  fvmptnn04if  19145  eltopspOLD  19214  tpsexOLD  19215  opnnei  19415  ordtbas2  19486  ordtrest2lem  19498  lmmo  19675  fincmp  19687  bwth  19704  txbas  19831  ptcnplem  19885  tx2ndc  19915  hmphtr  20047  fbun  20104  filcon  20147  ptcmplem5  20319  cnextcn  20330  utoptop  20500  restutopopn  20504  ucncn  20551  metustOLD  20833  metust  20834  cfilucfilOLD  20835  cfilucfil  20836  elcncf1di  21162  xrhmeo  21209  phtpycc  21254  copco  21281  pcohtpylem  21282  pcopt  21285  pcopt2  21286  ovolval  21648  iunmbl2  21730  itg2splitlem  21918  cpnfval  22098  plyval  22353  fta1  22466  aaliou2b  22499  ulmdvlem3  22559  radcnvlem2  22571  dvradcnv  22578  reeff1o  22604  sincosq1lem  22651  sincosq2sgn  22653  sincosq4sgn  22655  sinq12ge0  22662  logrncl  22711  eflog  22720  cxpge0  22820  atanf  22967  atanbnd  23013  lgsne0  23364  mul2sq  23396  pntibnd  23534  ostth  23580  mptelee  23902  axlowdimlem9  23957  axlowdimlem12  23960  axcontlem2  23972  axcontlem12  23982  isusgra0  24051  usgraop  24054  usgraedg4  24091  nbusgra  24132  nbgranself2  24140  wlkn0  24231  wlkcpr  24233  wlkntrllem3  24267  spthonepeq  24293  wlkdvspth  24314  cyclnspth  24335  3v3e3cycl2  24368  3v3e3cycl  24369  4cycl4dv  24371  2wlkeq  24411  usg2wlkeq  24412  clwwlknprop  24476  clwwisshclww  24511  wlklenvclwlk  24543  2wlkonot3v  24579  2spthonot3v  24580  2spontn0vne  24591  vdgrf  24602  usgfiregdegfi  24615  nbhashuvtx1  24619  eupath2lem1  24681  frgra3vlem1  24704  frgra3vlem2  24705  frgrancvvdeqlem2  24736  frgrancvvdeqlem3  24737  frgrancvvdeqlemB  24743  frgrancvvdeqlemC  24744  frgrawopreglem5  24753  usgreghash2spot  24774  frgrareg  24822  frgraregord013  24823  friendshipgt3  24826  isgrpo  24902  ismgm  25026  isrngo  25084  rngoablo2  25128  rngoueqz  25136  isdivrngo  25137  vci  25145  vcex  25177  nmogtmnf  25389  siilem1  25470  siii  25472  ajmoi  25478  bcsiALT  25800  hhcms  25824  ocval  25902  hsupval  25956  omlsilem  26024  h1de2bi  26176  h1de2ctlem  26177  hosubeq0i  26449  adjmo  26455  nmopgtmnf  26491  nlfnval  26504  nmcopex  26652  nmcfnex  26676  riesz4i  26686  riesz1  26688  riesz2  26689  opsqrlem1  26763  superpos  26977  hatomistici  26985  chpssati  26986  mdsymlem3  27028  mdsymi  27034  3o1cs  27073  3o2cs  27074  3o3cs  27075  ffsrn  27252  fpwrelmap  27256  ordtrest2NEWlem  27568  qqhval2  27627  logb1  27687  esumfsup  27744  esumcvg  27760  cntnevol  27867  ddemeas  27876  dya2icoseg2  27917  dya2iocnei  27921  eulerpartlems  27967  eulerpartlemgvv  27983  eulerpart  27989  cndprobprob  28045  ballotlemsdom  28118  ballotth  28144  sgn3da  28148  igamf  28261  igamcl  28262  txpcon  28345  ghomgrp  28533  setinds  28815  dfon2lem7  28826  dfon2lem8  28827  nnsinds  28902  nn0sinds  28903  poseq  28938  soseq  28939  wfrlem4  28951  wfrlem12  28959  wfrlem16  28963  wfr2  28965  frrlem4  28995  frrlem11  29004  nodenselem4  29049  nocvxminlem  29055  nocvxmin  29056  pprodss4v  29139  fullfunfv  29202  altxpsspw  29232  funtransport  29286  fvtransport  29287  funray  29395  fvray  29396  funline  29397  fvline  29399  bpolydiflem  29421  bpoly3  29425  bpoly4  29426  bisym1  29489  onsucconi  29507  onsucsuccmpi  29513  wl-lem-nexmo  29621  ismblfin  29660  itg2addnclem  29671  dvasin  29708  finminlem  29741  sdclem2  29866  totbndbnd  29916  exidresid  29972  isdrngo1  29990  isdrngo2  29992  ispridl2  30066  prtlem11  30239  mptfcl  30284  fphpd  30382  elmnc  30718  itgoval  30743  arearect  30816  lcmledvds  30833  pm11.71  30909  iotavalsb  30946  sbiota1  30947  cncficcgt0  31255  stoweidlem3  31331  stoweidlem17  31345  rexrsb  31669  raaan2  31675  afv0nbfvbi  31731  afvfv0bi  31732  afveu  31733  fnbrafvb  31734  afvres  31752  tz6.12-afv  31753  dmfcoafv  31755  afvco2  31756  aovprc  31768  aovrcl  31769  aovmpt4g  31781  2ffzoeq  31836  usgpredgv  31894  usgpredgvALT  31895  islinindfis  32149  secval  32240  cscval  32241  cotval  32242  2uasbanh  32432  eel0TT  32590  eelT00  32591  eelTTT  32592  eelT11  32594  eelT12  32598  eelTT1  32600  eelT01  32601  eel0T1  32602  eelTT  32666  uunT1p1  32676  uun121  32678  uun121p1  32679  un2122  32685  uunTT1  32688  uunTT1p1  32689  uunTT1p2  32690  uunT11  32691  uunT11p1  32692  uunT11p2  32693  uunT12  32694  uunT12p1  32695  uunT12p2  32696  uunT12p3  32697  uunT12p4  32698  uunT12p5  32699  uun111  32700  3anidm12p2  32702  uun123  32703  3impdirp1  32711  undif3VD  32780  ax6e2ndeqVD  32807  2uasbanhVD  32809  ax6e2ndeqALT  32829  iunconlem2  32833  sineq0ALT  32835  bnj945  32929  bnj1379  32986  bnj1459  32998  bnj557  33056  bnj571  33061  bnj849  33080  bnj964  33098  bnj978  33104  bnj1018  33117  bnj1020  33118  bnj1033  33122  bnj1175  33157  bnj1398  33187  bnj1417  33194  bnj1523  33224  bj-equsexv  33412  bj-equsal2  33497  bj-xpima1snALT  33613  lkr0f  33909  hl2at  34219  dalemswapyz  34470  pclfinclN  34764  osumcllem11N  34780  pexmidlem8N  34791  ltrnnid  34950
  Copyright terms: Public domain W3C validator