MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  sylbir 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
sylbir.2
Assertion
Ref Expression
sylbir

Proof of Theorem sylbir
StepHypRef Expression
1 sylbir.1 . . 3
21biimpri 206 . 2
3 sylbir.2 . 2
42, 3syl 16 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  <->wb 184
This theorem is referenced by:  3imtr3i  265  ex  434  3ori  1288  19.38  1662  19.35  1687  equsex  2038  nfeqf2  2041  sbi2  2134  ax12eq  2271  ax12el  2272  mo2v  2289  mo2vOLD  2290  mo2vOLDOLD  2291  mo2OLD  2334  2mo  2373  2moOLD  2374  axie2  2430  bm1.1OLD  2441  necon1bi  2690  necon1i  2699  sbhypf  3156  vtocl2  3162  vtocl3  3163  reu6  3288  uneqin  3748  inelcm  3881  difin0ss  3894  difprsn1  4166  tppreqb  4171  unissint  4311  intminss  4313  iununi  4415  bm1.3ii  4576  eusv2nf  4650  reusv3i  4659  reuxfr2d  4675  moabex  4711  copsex2g  4740  opelopabt  4764  eqrelrel  5109  opeliunxp2  5146  opelrn  5239  issref  5385  ssxpb  5446  xpima  5454  xpimasn  5457  dmsn0el  5482  relcoi2  5540  iotanul  5571  dffv2  5946  fnfvrnss  6059  fressnfv  6085  fconst5  6128  fconstfvOLD  6134  f1mpt  6169  isocnv3  6228  f1owe  6249  ovprc  6326  onminesb  6633  onminsb  6634  onintrab  6636  onnminsb  6639  onsucuni2  6669  tfindsg2  6696  zfrep6  6768  fo1stres  6824  fo2ndres  6825  bropopvvv  6880  frxp  6910  mpt2xopoveqd  6968  reldmtpos  6982  tfrlem5  7068  tfrlem9  7073  tfr2  7086  rdgsuc  7109  oaordi  7214  oeordi  7255  omopthi  7325  fvmptmap  7475  mptelixpg  7526  ener  7582  domtr  7588  snfi  7616  unen  7618  xpf1o  7699  mapen  7701  unxpdomlem3  7746  isinf  7753  frfi  7785  unblem1  7792  unfi  7807  fofinf1o  7821  fsuppun  7868  inf3lem2  8067  inf3lem5  8070  cantnfp1lem1  8118  cantnfp1lem3  8120  cantnfp1lem1OLD  8144  cantnfp1lem3OLD  8146  tcmin  8193  r1ordg  8217  r1ord  8219  rankr1ai  8237  r1val3  8277  bndrank  8280  unbndrank  8281  rankr1b  8303  rankxplim3  8320  tcrank  8323  xpnum  8353  cardmin2  8400  infxpenlem  8412  fseqen  8429  dfac8clem  8434  alephsson  8502  alephfp  8510  dfac4  8524  kmlem6  8556  kmlem8  8558  kmlem9  8559  infpssr  8709  fin1a2lem12  8812  axcc4  8840  axcc4dom  8842  ac6s2  8887  zornn0g  8906  cardidg  8944  unsnen  8949  pwcfsdom  8979  cfpwsdom  8980  gchpwdom  9069  r1tskina  9181  intgru  9213  indpi  9306  nqereu  9328  supsrlem  9509  letrii  9730  infmrcl  10547  dfnn3  10575  zaddcl  10929  uzindOLD  10982  nn0ind  10984  fnn0ind  10988  ublbneg  11195  nn01to3  11204  fz0  11730  fzo1fzo0n0  11864  elfzom1elp1fzo  11883  fzo0end  11904  elfznelfzo  11915  fzind2  11924  injresinjlem  11925  fleqceilz  11981  fsuppmapnn0fiubex  12098  faclbnd4lem1  12371  hashinf  12410  hasheqf1oi  12424  hashgt0elex  12466  hashfacen  12503  hash2prde  12516  lswcl  12589  lswccats1fst  12639  swrdlsw  12677  swrdswrdlem  12684  swrdccatin12lem3  12715  swrdccat3  12717  swrdccat3blem  12720  cshwsublen  12767  cshwidxmod  12774  repswcshw  12780  cshw1  12790  rediv  12964  imdiv  12971  sqrt0  13075  fsump1i  13584  modfsummods  13607  cos1bnd  13922  sinltx  13924  rpnnen2lem1  13948  rpnnen2lem2  13949  rpnnen2  13959  odd2np1  14046  gcdcllem1  14149  gcdaddmlem  14166  algfx  14209  odzval  14318  odzdvds  14322  opoe  14335  omoe  14336  opeo  14337  omeo  14338  prmreclem5  14438  mul4sq  14472  imasaddfnlem  14925  mreexexlem4d  15044  joindmss  15637  meetdmss  15651  gictr  16323  cntzval  16359  symg2bas  16423  efgsfo  16757  efgrelexlemb  16768  dprddomcld  17032  dprdsubg  17071  dprd2da  17091  lssacs  17613  cnfldinv  18449  ocvval  18698  dmatmul  18999  mdetfval1  19092  mndifsplit  19138  fvmptnn04if  19350  eltopspOLD  19419  tpsexOLD  19420  opnnei  19621  ordtbas2  19692  ordtrest2lem  19704  lmmo  19881  fincmp  19893  bwth  19910  txbas  20068  ptcnplem  20122  tx2ndc  20152  hmphtr  20284  fbun  20341  filcon  20384  ptcmplem5  20556  cnextcn  20567  utoptop  20737  ucncn  20788  metustOLD  21070  metust  21071  cfilucfilOLD  21072  cfilucfil  21073  elcncf1di  21399  xrhmeo  21446  phtpycc  21491  copco  21518  pcohtpylem  21519  pcopt  21522  pcopt2  21523  ovolval  21885  iunmbl2  21967  itg2splitlem  22155  cpnfval  22335  plyval  22590  fta1  22704  aaliou2b  22737  ulmdvlem3  22797  radcnvlem2  22809  dvradcnv  22816  reeff1o  22842  sincosq1lem  22890  sincosq2sgn  22892  sincosq4sgn  22894  sinq12ge0  22901  logrncl  22955  eflog  22964  cxpge0  23064  atanf  23211  atanbnd  23257  lgsne0  23608  mul2sq  23640  pntibnd  23778  ostth  23824  mptelee  24198  axlowdimlem9  24253  axlowdimlem12  24256  axcontlem2  24268  axcontlem12  24278  isusgra0  24347  usgraop  24350  usgraedg4  24387  nbusgra  24428  nbgranself2  24436  wlkn0  24527  wlkcpr  24529  wlkntrllem3  24563  spthonepeq  24589  wlkdvspth  24610  cyclnspth  24631  3v3e3cycl2  24664  3v3e3cycl  24665  4cycl4dv  24667  2wlkeq  24707  usg2wlkeq  24708  clwwlknprop  24772  clwwisshclww  24807  wlklenvclwlk  24839  2wlkonot3v  24875  2spthonot3v  24876  2spontn0vne  24887  vdgrf  24898  usgfiregdegfi  24911  nbhashuvtx1  24915  eupath2lem1  24977  frgra3vlem1  25000  frgra3vlem2  25001  frgrancvvdeqlem2  25031  frgrancvvdeqlem3  25032  frgrancvvdeqlemB  25038  frgrancvvdeqlemC  25039  frgrawopreglem5  25048  usgreghash2spot  25069  frgrareg  25117  frgraregord013  25118  friendshipgt3  25121  isgrpo  25198  ismgmOLD  25322  isrngo  25380  rngoablo2  25424  rngoueqz  25432  isdivrngo  25433  vci  25441  vcex  25473  nmogtmnf  25685  siilem1  25766  siii  25768  ajmoi  25774  bcsiALT  26096  hhcms  26120  ocval  26198  hsupval  26252  omlsilem  26320  h1de2bi  26472  h1de2ctlem  26473  hosubeq0i  26745  adjmo  26751  nmopgtmnf  26787  nlfnval  26800  nmcopex  26948  nmcfnex  26972  riesz4i  26982  riesz1  26984  riesz2  26985  opsqrlem1  27059  superpos  27273  hatomistici  27281  chpssati  27282  mdsymlem3  27324  3o1cs  27369  3o2cs  27370  3o3cs  27371  spc2ed  27372  ffsrn  27552  fpwrelmap  27556  ordtrest2NEWlem  27904  qqhval2  27963  logb1  28019  esumfsup  28076  esumcvg  28092  cntnevol  28199  ddemeas  28208  dya2icoseg2  28249  dya2iocnei  28253  eulerpartlems  28299  eulerpartlemgvv  28315  eulerpart  28321  cndprobprob  28377  ballotlemsdom  28450  ballotth  28476  sgn3da  28480  igamf  28593  igamcl  28594  txpcon  28677  msubco  28891  mclsax  28929  ghomgrp  29030  setinds  29210  dfon2lem7  29221  dfon2lem8  29222  nnsinds  29297  nn0sinds  29298  poseq  29333  soseq  29334  wfrlem4  29346  wfrlem12  29354  wfrlem16  29358  wfr2  29360  frrlem4  29390  frrlem11  29399  nodenselem4  29444  nocvxminlem  29450  nocvxmin  29451  pprodss4v  29534  fullfunfv  29597  altxpsspw  29627  funtransport  29681  fvtransport  29682  funray  29790  fvray  29791  funline  29792  fvline  29794  bpolydiflem  29816  bpoly3  29820  bpoly4  29821  bisym1  29884  onsucconi  29902  onsucsuccmpi  29908  wl-lem-nexmo  30016  ismblfin  30055  itg2addnclem  30066  dvasin  30103  finminlem  30136  sdclem2  30235  totbndbnd  30285  exidresid  30341  isdrngo1  30359  isdrngo2  30361  ispridl2  30435  prtlem11  30607  mptfcl  30652  fphpd  30750  elmnc  31085  itgoval  31110  arearect  31183  nanorxor  31185  lcmledvds  31205  pm11.71  31303  iotavalsb  31340  sbiota1  31341  ioodvbdlimc1lem2  31729  ioodvbdlimc2lem  31731  stoweidlem3  31785  stoweidlem17  31799  fourierdlem42  31931  fourierdlem48  31937  fourierdlem50  31939  fourierdlem51  31940  fourierdlem76  31965  fourierdlem83  31972  fourierdlem87  31976  rexrsb  32174  raaan2  32180  afv0nbfvbi  32236  afvfv0bi  32237  afveu  32238  fnbrafvb  32239  afvres  32257  tz6.12-afv  32258  dmfcoafv  32260  afvco2  32261  aovprc  32273  aovrcl  32274  aovmpt4g  32286  2ffzoeq  32341  usgpredgv  32399  usgpredgvALT  32400  ovn0ssdmfun  32455  islinindfis  33050  secval  33141  cscval  33142  cotval  33143  2uasbanh  33334  eel0TT  33492  eelT00  33493  eelTTT  33494  eelT11  33496  eelT12  33500  eelTT1  33502  eelT01  33503  eel0T1  33504  eelTT  33568  uunT1p1  33578  uun121  33580  uun121p1  33581  un2122  33587  uunTT1  33590  uunTT1p1  33591  uunTT1p2  33592  uunT11  33593  uunT11p1  33594  uunT11p2  33595  uunT12  33596  uunT12p1  33597  uunT12p2  33598  uunT12p3  33599  uunT12p4  33600  uunT12p5  33601  uun111  33602  3anidm12p2  33604  uun123  33605  3impdirp1  33613  undif3VD  33682  ax6e2ndeqVD  33709  2uasbanhVD  33711  ax6e2ndeqALT  33731  iunconlem2  33735  sineq0ALT  33737  bnj945  33832  bnj1379  33889  bnj1459  33901  bnj557  33959  bnj571  33964  bnj849  33983  bnj964  34001  bnj978  34007  bnj1018  34020  bnj1020  34021  bnj1033  34025  bnj1175  34060  bnj1398  34090  bnj1417  34097  bnj1523  34127  bj-equsexv  34312  bj-equsexvv  34313  bj-equsal2  34398  bj-xpima1snALT  34514  lkr0f  34819  hl2at  35129  dalemswapyz  35380  pclfinclN  35674  osumcllem11N  35690  pexmidlem8N  35701  ltrnnid  35860
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
  Copyright terms: Public domain W3C validator