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

Theorem sylbir 218
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 211 . 2  |-  ( ph  ->  ps )
3 sylbir.2 . 2  |-  ( ps 
->  ch )
42, 3syl 17 1  |-  ( ph  ->  ch )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 189
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 190
This theorem is referenced by:  3imtr3i  273  ex  440  3ori  1332  19.38  1716  19.35  1744  equsex  2131  nfeqf2  2136  sbi2  2223  mo2v  2307  2mo  2381  axie2  2427  necon1bi  2652  necon1i  2657  sbhypf  3063  vtocl2  3070  vtocl3  3071  reu6  3195  uneqin  3662  inelcm  3787  difin0ss  3801  difprsn1  4077  tppreqb  4082  unissint  4229  intminss  4231  iununi  4338  bm1.3ii  4500  eusv2nf  4574  reusv3i  4583  reuxfr2d  4596  moabex  4632  copsex2g  4662  opelopabt  4686  eqrelrel  4914  opeliunxp2  4951  opelrn  5044  issref  5191  ssxpb  5249  xpima  5257  xpimasn  5260  dmsn0el  5284  relcoi2  5342  elsnxp  5357  iotanul  5540  dffv2  5922  fnfvrnss  6035  fressnfv  6063  fconst5  6107  fconstfvOLD  6113  f1mpt  6148  isocnv3  6209  f1owe  6230  ovprc  6306  onminesb  6613  onminsb  6614  onintrab  6616  onnminsb  6619  onsucuni2  6649  tfindsg2  6676  zfrep6  6749  fo1stres  6805  fo2ndres  6806  bropopvvv  6862  bropfvvvv  6864  frxp  6894  opeliunxp2f  6944  mpt2xopoveqd  6955  reldmtpos  6968  wfrlem4  7026  wfrlem12  7034  wfrlem16  7038  wfr2  7042  tfrlem5  7085  tfrlem9  7090  tfr2  7103  rdgsuc  7129  oaordi  7234  oeordi  7275  omopthi  7345  fvmptmap  7495  mptelixpg  7546  ener  7603  domtr  7609  snfi  7637  unen  7639  xpf1o  7721  mapen  7723  unxpdomlem3  7765  isinf  7772  frfi  7803  unblem1  7810  unfi  7825  fofinf1o  7839  fsuppun  7889  inf3lem2  8121  inf3lem5  8124  cantnfp1lem1  8170  cantnfp1lem3  8172  tcmin  8212  r1ordg  8236  r1ord  8238  rankr1ai  8256  r1val3  8296  bndrank  8299  unbndrank  8300  rankr1b  8322  rankxplim3  8339  tcrank  8342  xpnum  8372  cardmin2  8419  infxpenlem  8431  fseqen  8445  dfac8clem  8450  alephsson  8518  alephfp  8526  dfac4  8540  kmlem6  8572  kmlem8  8574  kmlem9  8575  infpssr  8725  fin1a2lem12  8828  axcc4  8856  axcc4dom  8858  ac6s2  8903  zornn0g  8922  cardidg  8960  unsnen  8965  pwcfsdom  8995  cfpwsdom  8996  gchpwdom  9082  r1tskina  9194  intgru  9226  indpi  9319  nqereu  9341  supsrlem  9522  letrii  9746  infmrclOLD  10582  dfnn3  10612  zaddcl  10967  nn0ind  11020  fnn0ind  11024  ublbneg  11238  nn01to3  11247  infmrp1  11624  fz0  11805  fzo1fzo0n0  11950  elfzom1elp1fzo  11974  fzo0end  11996  elfznelfzo  12007  fzind2  12016  injresinjlem  12018  fleqceilz  12075  nnsinds  12194  nn0sinds  12195  fsuppmapnn0fiubex  12198  faclbnd4lem1  12472  hashinf  12514  hasheqf1oi  12528  hashgt0elex  12572  hashfacen  12612  hash2prde  12626  hash2sspr  12639  swrdn0  12785  swrdlsw  12807  swrdswrdlem  12814  swrdccatin12lem3  12845  swrdccat3  12847  swrdccat3blem  12850  cshwsublen  12897  cshwidxmod  12904  repswcshw  12910  cshw1  12920  trclun  13089  dmtrclfv  13093  rediv  13205  imdiv  13212  sqrt0  13316  fsump1i  13841  modfsummods  13864  bpolydiflem  14118  bpoly3  14122  bpoly4  14123  cos1bnd  14252  sinltx  14254  rpnnen2lem1  14278  rpnnen2lem2  14279  rpnnen2  14289  odd2np1  14376  gcdcllem1  14484  gcdaddmlem  14503  algfx  14550  lcmledvds  14575  lcmsledvdsOLD  14596  lcmfunsnlem  14625  lcmfun  14629  coprmprod  14689  coprmproddvdslem  14690  odzval  14747  odzdvds  14751  odzvalOLD  14753  odzdvdsOLD  14757  opoe  14772  omoe  14773  opeo  14774  omeo  14775  prmreclem5  14875  mul4sq  14909  prmgaplem5  15036  prmgaplem6  15037  imasaddfnlem  15445  mreexexlem4d  15564  joindmss  16264  meetdmss  16278  gictr  16950  cntzval  16986  symg2bas  17050  efgsfo  17400  efgrelexlemb  17411  dprddomcld  17644  dprdsubg  17668  dprd2da  17686  lssacs  18201  cnfldinv  19010  ocvval  19241  dmatmul  19533  mdetfval1  19626  mndifsplit  19672  fvmptnn04if  19884  opnnei  20147  ordtbas2  20218  ordtrest2lem  20230  lmmo  20407  fincmp  20419  bwth  20436  txbas  20593  ptcnplem  20647  tx2ndc  20677  hmphtr  20809  fbun  20866  filcon  20909  ptcmplem5  21082  cnextcn  21093  utoptop  21260  ucncn  21311  metust  21584  cfilucfil  21585  elcncf1di  21938  xrhmeo  21985  phtpycc  22033  copco  22060  pcohtpylem  22061  pcopt  22064  pcopt2  22065  ovolval  22437  ovolvalOLD  22438  iunmbl2  22522  itg2splitlem  22718  cpnfval  22898  plyval  23159  fta1  23273  aaliou2b  23309  ulmdvlem3  23369  radcnvlem2  23381  dvradcnv  23388  reeff1o  23414  sincosq1lem  23464  sincosq2sgn  23466  sincosq4sgn  23468  sinq12ge0  23475  logrncl  23529  eflog  23538  cxpge0  23640  logb1  23718  atanf  23818  atanbnd  23864  igamf  23988  igamcl  23989  lgsne0  24273  mul2sq  24305  pntibnd  24443  ostth  24489  mptelee  24937  axlowdimlem9  24992  axlowdimlem12  24995  axcontlem2  25007  axcontlem12  25017  isusgra0  25086  usgraop  25089  usgraedg4  25126  nbusgra  25168  nbgranself2  25176  wlkn0  25267  wlkcpr  25269  wlkntrllem3  25303  spthonepeq  25329  wlkdvspth  25350  cyclnspth  25371  3v3e3cycl2  25404  3v3e3cycl  25405  4cycl4dv  25407  2wlkeq  25447  usg2wlkeq  25448  clwwlknprop  25512  clwwisshclww  25547  wlklenvclwlk  25579  2wlkonot3v  25615  2spthonot3v  25616  2spontn0vne  25627  vdgrf  25638  usgfiregdegfi  25651  nbhashuvtx1  25655  eupath2lem1  25717  frgra3vlem1  25740  frgra3vlem2  25741  frgrancvvdeqlem2  25771  frgrancvvdeqlem3  25772  frgrancvvdeqlemB  25778  frgrancvvdeqlemC  25779  frgrawopreglem5  25788  usgreghash2spot  25809  frgrareg  25857  frgraregord013  25858  friendshipgt3  25861  isgrpo  25936  ismgmOLD  26060  isrngo  26118  rngoablo2  26162  rngoueqz  26170  isdivrngo  26171  vci  26179  vcex  26211  nmogtmnf  26423  siilem1  26504  siii  26506  ajmoi  26512  bcsiALT  26844  hhcms  26868  ocval  26945  hsupval  26999  omlsilem  27067  h1de2bi  27219  h1de2ctlem  27220  hosubeq0i  27491  adjmo  27497  nmopgtmnf  27533  nlfnval  27546  nmcopex  27694  nmcfnex  27718  riesz4i  27728  riesz1  27730  riesz2  27731  opsqrlem1  27805  superpos  28019  hatomistici  28027  chpssati  28028  mdsymlem3  28070  3o1cs  28115  3o2cs  28116  3o3cs  28117  spc2ed  28118  brabgaf  28225  f1mptrn  28241  ffsrn  28322  fpwrelmap  28326  ordtrest2NEWlem  28735  qqhval2  28793  esumfsup  28898  esumcvg  28914  cntnevol  29057  ddemeas  29065  dya2icoseg2  29106  dya2iocnei  29110  eulerpartlems  29199  eulerpartlemgvv  29215  eulerpart  29221  cndprobprob  29277  ballotlemsdom  29350  ballotth  29376  ballotlemsdomOLD  29388  ballotthOLD  29414  sgn3da  29418  bnj945  29591  bnj1379  29648  bnj1459  29660  bnj557  29718  bnj571  29723  bnj849  29742  bnj964  29760  bnj978  29766  bnj1018  29779  bnj1020  29780  bnj1033  29784  bnj1175  29819  bnj1398  29849  bnj1417  29856  bnj1523  29886  txpcon  29961  msubco  30175  mclsax  30213  ghomgrp  30314  setinds  30430  dfon2lem7  30441  dfon2lem8  30442  poseq  30497  soseq  30498  frrlem4  30523  frrlem11  30532  nodenselem4  30579  nocvxminlem  30585  nocvxmin  30586  pprodss4v  30657  fullfunfv  30720  altxpsspw  30750  funtransport  30804  fvtransport  30805  funray  30913  fvray  30914  funline  30915  fvline  30917  finminlem  30980  bisym1  31085  onsucconi  31103  onsucsuccmpi  31109  bj-alcomexcom  31281  bj-equsal2  31429  bj-xpima1snALT  31552  f1omptsnlem  31740  mptsnunlem  31742  iooelexlt  31767  relowlpssretop  31769  rdgeqoa  31775  wl-lem-nexmo  31898  ptrecube  31942  poimirlem26  31968  poimirlem30  31972  poimir  31975  ismblfin  31983  itg2addnclem  31995  dvasin  32030  sdclem2  32073  totbndbnd  32123  exidresid  32179  isdrngo1  32197  isdrngo2  32199  ispridl2  32273  prtlem11  32440  ax12eq  32514  ax12el  32515  lkr0f  32662  hl2at  32972  dalemswapyz  33223  pclfinclN  33517  osumcllem11N  33533  pexmidlem8N  33544  ltrnnid  33703  mptfcl  35564  fphpd  35661  elmnc  35997  itgoval  36029  arearect  36102  nanorxor  36654  pm11.71  36748  iotavalsb  36785  sbiota1  36786  2uasbanh  36929  eel0TT  37084  eelT00  37085  eelTTT  37086  eelT11  37087  eelT12  37091  eelTT1  37092  eelT01  37093  eel0T1  37094  eelTT  37155  uunT1p1  37165  uun121  37167  uun121p1  37168  un2122  37174  uunTT1  37177  uunTT1p1  37178  uunTT1p2  37179  uunT11  37180  uunT11p1  37181  uunT11p2  37182  uunT12  37183  uunT12p1  37184  uunT12p2  37185  uunT12p3  37186  uunT12p4  37187  uunT12p5  37188  uun111  37189  3anidm12p2  37191  uun123  37192  3impdirp1  37200  undif3VD  37276  ax6e2ndeqVD  37303  2uasbanhVD  37305  ax6e2ndeqALT  37325  iunconlem2  37329  sineq0ALT  37331  ioodvbdlimc1lem2  37846  ioodvbdlimc1lem2OLD  37848  ioodvbdlimc2lem  37850  ioodvbdlimc2lemOLD  37851  stoweidlem3  37920  stoweidlem17  37934  fourierdlem42  38069  fourierdlem42OLD  38070  fourierdlem48  38075  fourierdlem50  38077  fourierdlem51  38078  fourierdlem76  38103  fourierdlem83  38110  fourierdlem87  38114  hoidmvval0  38472  rexrsb  38681  raaan2  38687  afv0nbfvbi  38744  afvfv0bi  38745  afveu  38746  fnbrafvb  38747  afvres  38765  tz6.12-afv  38766  dmfcoafv  38768  afvco2  38769  aovprc  38781  aovrcl  38782  aovmpt4g  38794  fzopred  38810  pfxccat3  39060  pfxccat3a  39063  falseral0  39079  n0snor2el  39089  fun2dmnop  39121  2ffzoeq  39158  structgrssvtx  39224  structgrssiedg  39225  lpvtx  39257  umgredg  39329  nbuhgr  39513  nbumgr  39517  nbuhgr2vtx1edgblem  39521  nbgr0vtxlem  39525  nbgr1vtx  39528  uvtxa01vtx0  39571  cusgrsizeinds  39615  sizusglecusglem2  39625  uhgrvd00  39673  fusgrregdegfi  39688  rusgr1vtxlem  39704  1wlkn0  39737  1wlk1walk  39749  upgr1wlkwlk  39752  1wlkdlem2  39778  1wlkdlem4  39780  spthonepeq-av  39836  31wlkdlem6  39958  usgpredgv  40036  usgpredgvALT  40037  ovn0ssdmfun  40092  islinindfis  40567  secval  40792  cscval  40793  cotval  40794
  Copyright terms: Public domain W3C validator