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  432  3ori  1286  19.38  1670  19.35  1695  equsex  2044  nfeqf2  2047  sbi2  2138  mo2v  2225  mo2vOLD  2226  mo2vOLDOLD  2227  2mo  2304  2moOLD  2305  axie2  2355  bm1.1OLD  2366  necon1bi  2615  necon1i  2624  sbhypf  3081  vtocl2  3087  vtocl3  3088  reu6  3213  uneqin  3674  inelcm  3797  difin0ss  3810  difprsn1  4080  tppreqb  4085  unissint  4224  intminss  4226  iununi  4331  bm1.3ii  4491  eusv2nf  4563  reusv3i  4572  reuxfr2d  4585  moabex  4621  copsex2g  4649  opelopabt  4673  eqrelrel  5017  opeliunxp2  5054  opelrn  5147  issref  5293  ssxpb  5351  xpima  5359  xpimasn  5362  dmsn0el  5385  relcoi2  5443  iotanul  5475  dffv2  5847  fnfvrnss  5961  fressnfv  5987  fconst5  6031  fconstfvOLD  6035  f1mpt  6070  isocnv3  6129  f1owe  6150  ovprc  6226  onminesb  6532  onminsb  6533  onintrab  6535  onnminsb  6538  onsucuni2  6568  tfindsg2  6595  zfrep6  6667  fo1stres  6723  fo2ndres  6724  bropopvvv  6779  frxp  6809  mpt2xopoveqd  6867  reldmtpos  6881  tfrlem5  6967  tfrlem9  6972  tfr2  6985  rdgsuc  7008  oaordi  7113  oeordi  7154  omopthi  7224  fvmptmap  7374  mptelixpg  7425  ener  7481  domtr  7487  snfi  7515  unen  7517  xpf1o  7598  mapen  7600  unxpdomlem3  7642  isinf  7649  frfi  7680  unblem1  7687  unfi  7702  fofinf1o  7716  fsuppun  7763  inf3lem2  7960  inf3lem5  7963  cantnfp1lem1  8010  cantnfp1lem3  8012  cantnfp1lem1OLD  8036  cantnfp1lem3OLD  8038  tcmin  8085  r1ordg  8109  r1ord  8111  rankr1ai  8129  r1val3  8169  bndrank  8172  unbndrank  8173  rankr1b  8195  rankxplim3  8212  tcrank  8215  xpnum  8245  cardmin2  8292  infxpenlem  8304  fseqen  8321  dfac8clem  8326  alephsson  8394  alephfp  8402  dfac4  8416  kmlem6  8448  kmlem8  8450  kmlem9  8451  infpssr  8601  fin1a2lem12  8704  axcc4  8732  axcc4dom  8734  ac6s2  8779  zornn0g  8798  cardidg  8836  unsnen  8841  pwcfsdom  8871  cfpwsdom  8872  gchpwdom  8959  r1tskina  9071  intgru  9103  indpi  9196  nqereu  9218  supsrlem  9399  letrii  9620  infmrcl  10438  dfnn3  10466  zaddcl  10821  nn0ind  10874  fnn0ind  10878  ublbneg  11085  nn01to3  11094  fz0  11622  fzo1fzo0n0  11759  elfzom1elp1fzo  11782  fzo0end  11803  elfznelfzo  11814  fzind2  11823  injresinjlem  11824  fleqceilz  11881  fsuppmapnn0fiubex  12001  faclbnd4lem1  12273  hashinf  12312  hasheqf1oi  12326  hashgt0elex  12370  hashfacen  12407  hash2prde  12420  swrdn0  12566  swrdlsw  12588  swrdswrdlem  12595  swrdccatin12lem3  12626  swrdccat3  12628  swrdccat3blem  12631  cshwsublen  12678  cshwidxmod  12685  repswcshw  12691  cshw1  12701  trclun  12852  dmtrclfv  12856  rediv  12966  imdiv  12973  sqrt0  13077  fsump1i  13586  modfsummods  13609  cos1bnd  13924  sinltx  13926  rpnnen2lem1  13950  rpnnen2lem2  13951  rpnnen2  13961  odd2np1  14048  gcdcllem1  14151  gcdaddmlem  14168  algfx  14211  odzval  14320  odzdvds  14324  opoe  14337  omoe  14338  opeo  14339  omeo  14340  prmreclem5  14440  mul4sq  14474  imasaddfnlem  14935  mreexexlem4d  15054  joindmss  15754  meetdmss  15768  gictr  16440  cntzval  16476  symg2bas  16540  efgsfo  16874  efgrelexlemb  16885  dprddomcld  17145  dprdsubg  17184  dprd2da  17204  lssacs  17726  cnfldinv  18562  ocvval  18789  dmatmul  19084  mdetfval1  19177  mndifsplit  19223  fvmptnn04if  19435  eltopspOLD  19504  tpsexOLD  19505  opnnei  19707  ordtbas2  19778  ordtrest2lem  19790  lmmo  19967  fincmp  19979  bwth  19996  txbas  20153  ptcnplem  20207  tx2ndc  20237  hmphtr  20369  fbun  20426  filcon  20469  ptcmplem5  20641  cnextcn  20652  utoptop  20822  ucncn  20873  metustOLD  21155  metust  21156  cfilucfilOLD  21157  cfilucfil  21158  elcncf1di  21484  xrhmeo  21531  phtpycc  21576  copco  21603  pcohtpylem  21604  pcopt  21607  pcopt2  21608  ovolval  21970  iunmbl2  22052  itg2splitlem  22240  cpnfval  22420  plyval  22675  fta1  22789  aaliou2b  22822  ulmdvlem3  22882  radcnvlem2  22894  dvradcnv  22901  reeff1o  22927  sincosq1lem  22975  sincosq2sgn  22977  sincosq4sgn  22979  sinq12ge0  22986  logrncl  23040  eflog  23049  cxpge0  23151  logb1  23227  atanf  23327  atanbnd  23373  lgsne0  23725  mul2sq  23757  pntibnd  23895  ostth  23941  mptelee  24319  axlowdimlem9  24374  axlowdimlem12  24377  axcontlem2  24389  axcontlem12  24399  isusgra0  24468  usgraop  24471  usgraedg4  24508  nbusgra  24549  nbgranself2  24557  wlkn0  24648  wlkcpr  24650  wlkntrllem3  24684  spthonepeq  24710  wlkdvspth  24731  cyclnspth  24752  3v3e3cycl2  24785  3v3e3cycl  24786  4cycl4dv  24788  2wlkeq  24828  usg2wlkeq  24829  clwwlknprop  24893  clwwisshclww  24928  wlklenvclwlk  24960  2wlkonot3v  24996  2spthonot3v  24997  2spontn0vne  25008  vdgrf  25019  usgfiregdegfi  25032  nbhashuvtx1  25036  eupath2lem1  25098  frgra3vlem1  25121  frgra3vlem2  25122  frgrancvvdeqlem2  25152  frgrancvvdeqlem3  25153  frgrancvvdeqlemB  25159  frgrancvvdeqlemC  25160  frgrawopreglem5  25169  usgreghash2spot  25190  frgrareg  25238  frgraregord013  25239  friendshipgt3  25242  isgrpo  25315  ismgmOLD  25439  isrngo  25497  rngoablo2  25541  rngoueqz  25549  isdivrngo  25550  vci  25558  vcex  25590  nmogtmnf  25802  siilem1  25883  siii  25885  ajmoi  25891  bcsiALT  26213  hhcms  26237  ocval  26315  hsupval  26369  omlsilem  26437  h1de2bi  26589  h1de2ctlem  26590  hosubeq0i  26861  adjmo  26867  nmopgtmnf  26903  nlfnval  26916  nmcopex  27064  nmcfnex  27088  riesz4i  27098  riesz1  27100  riesz2  27101  opsqrlem1  27175  superpos  27389  hatomistici  27397  chpssati  27398  mdsymlem3  27440  3o1cs  27486  3o2cs  27487  3o3cs  27488  spc2ed  27489  brabgaf  27595  elsnxp  27603  f1mptrn  27612  ffsrn  27702  fpwrelmap  27706  ordtrest2NEWlem  28058  qqhval2  28116  esumfsup  28218  esumcvg  28234  cntnevol  28355  ddemeas  28364  dya2icoseg2  28405  dya2iocnei  28409  eulerpartlems  28482  eulerpartlemgvv  28498  eulerpart  28504  cndprobprob  28560  ballotlemsdom  28633  ballotth  28659  sgn3da  28663  igamf  28782  igamcl  28783  txpcon  28866  msubco  29080  mclsax  29118  ghomgrp  29219  setinds  29375  dfon2lem7  29386  dfon2lem8  29387  nnsinds  29462  nn0sinds  29463  poseq  29498  soseq  29499  wfrlem4  29511  wfrlem12  29519  wfrlem16  29523  wfr2  29525  frrlem4  29555  frrlem11  29564  nodenselem4  29609  nocvxminlem  29615  nocvxmin  29616  pprodss4v  29687  fullfunfv  29750  altxpsspw  29780  funtransport  29834  fvtransport  29835  funray  29943  fvray  29944  funline  29945  fvline  29947  bpolydiflem  29969  bpoly3  29973  bpoly4  29974  bisym1  30037  onsucconi  30055  onsucsuccmpi  30061  wl-lem-nexmo  30181  ismblfin  30220  itg2addnclem  30232  dvasin  30269  finminlem  30302  sdclem2  30401  totbndbnd  30451  exidresid  30507  isdrngo1  30525  isdrngo2  30527  ispridl2  30601  prtlem11  30773  mptfcl  30818  fphpd  30915  elmnc  31253  itgoval  31278  arearect  31351  nanorxor  31353  lcmledvds  31373  pm11.71  31471  iotavalsb  31508  sbiota1  31509  ioodvbdlimc1lem2  31895  ioodvbdlimc2lem  31897  stoweidlem3  31951  stoweidlem17  31965  fourierdlem42  32097  fourierdlem48  32103  fourierdlem50  32105  fourierdlem51  32106  fourierdlem76  32131  fourierdlem83  32138  fourierdlem87  32142  rexrsb  32340  raaan2  32346  afv0nbfvbi  32402  afvfv0bi  32403  afveu  32404  fnbrafvb  32405  afvres  32423  tz6.12-afv  32424  dmfcoafv  32426  afvco2  32427  aovprc  32439  aovrcl  32440  aovmpt4g  32452  pfxccat3  32601  pfxccat3a  32604  2ffzoeq  32661  usgpredgv  32717  usgpredgvALT  32718  ovn0ssdmfun  32773  islinindfis  33250  secval  33477  cscval  33478  cotval  33479  2uasbanh  33674  eel0TT  33832  eelT00  33833  eelTTT  33834  eelT11  33836  eelT12  33840  eelTT1  33842  eelT01  33843  eel0T1  33844  eelTT  33908  uunT1p1  33918  uun121  33920  uun121p1  33921  un2122  33927  uunTT1  33930  uunTT1p1  33931  uunTT1p2  33932  uunT11  33933  uunT11p1  33934  uunT11p2  33935  uunT12  33936  uunT12p1  33937  uunT12p2  33938  uunT12p3  33939  uunT12p4  33940  uunT12p5  33941  uun111  33942  3anidm12p2  33944  uun123  33945  3impdirp1  33953  undif3VD  34029  ax6e2ndeqVD  34056  2uasbanhVD  34058  ax6e2ndeqALT  34078  iunconlem2  34082  sineq0ALT  34084  bnj945  34179  bnj1379  34236  bnj1459  34248  bnj557  34306  bnj571  34311  bnj849  34330  bnj964  34348  bnj978  34354  bnj1018  34367  bnj1020  34368  bnj1033  34372  bnj1175  34407  bnj1398  34437  bnj1417  34444  bnj1523  34474  bj-equsexv  34659  bj-equsexvv  34660  bj-equsal2  34745  bj-xpima1snALT  34862  ax12eq  35084  ax12el  35085  lkr0f  35232  hl2at  35542  dalemswapyz  35793  pclfinclN  36087  osumcllem11N  36103  pexmidlem8N  36114  ltrnnid  36273
  Copyright terms: Public domain W3C validator