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

Theorem sylbir 226
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 219 . 2 (𝜑𝜓)
3 sylbir.2 . 2 (𝜓𝜒)
42, 3syl 17 1 (𝜑𝜒)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 197
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 198
This theorem is referenced by:  3imtr3i  282  ex  399  3expa  1140  3ori  1541  19.38  1923  19.35  1967  equsex  2461  nfeqf2  2466  nfeqf2OLD  2467  sbi2  2554  nexmo  2640  dfmo  2651  2mo  2726  axie2  2790  necon1bi  3017  necon1i  3022  sbhypf  3458  vtocl2  3465  vtocl3  3466  reu6  3604  rabssrabd  3897  uneqin  4091  difin0ss  4158  inelcm  4240  falseral0  4285  difprsn1  4532  tppreqb  4537  n0snor2el  4563  unissint  4704  intminss  4706  iununi  4813  bm1.3ii  4991  eusv2nf  5077  reusv3i  5086  reuxfr2d  5101  moabex  5130  copsex2g  5160  opelopabt  5195  eqrelrel  5436  opeliunxp2  5475  opelrn  5571  idrefOLD  5733  ssxpb  5792  xpima  5800  xpimasn  5803  dmsn0el  5828  relcoi2  5890  elsnxp  5904  iotanul  6088  dffv2  6501  fnfvrnss  6621  fressnfv  6660  fconst5  6705  f1mpt  6751  isocnv3  6815  f1owe  6836  ovprc  6920  onminesb  7237  onminsb  7238  onintrab  7240  onnminsb  7243  onsucuni2  7273  tfindsg2  7300  zfrep6  7373  fo1stres  7433  fo2ndres  7434  bropopvvv  7498  bropfvvvv  7500  frxp  7530  opeliunxp2f  7580  mpt2xopoveqd  7591  reldmtpos  7604  wfrlem4  7662  wfrlem4OLD  7663  wfrlem12  7671  wfrlem16  7675  wfr2  7679  tfrlem5  7721  tfrlem9  7726  tfr2  7739  rdgsuc  7765  oaordi  7872  oeordi  7913  omopthi  7983  fvmptmap  8138  mptelixpg  8191  ener  8248  domtr  8254  snfi  8286  unen  8288  xpf1o  8370  mapen  8372  unxpdomlem3  8414  isinf  8421  frfi  8453  unblem1  8460  unfi  8475  fofinf1o  8489  fsuppun  8542  inf3lem2  8782  inf3lem5  8785  cantnfp1lem1  8831  cantnfp1lem3  8833  tcmin  8873  r1ordg  8897  r1ord  8899  rankr1ai  8917  r1val3  8957  bndrank  8960  unbndrank  8961  rankr1b  8983  rankxplim3  9000  tcrank  9003  xpnum  9069  cardmin2  9116  infxpenlem  9128  fseqen  9142  dfac8clem  9147  alephsson  9215  alephfp  9223  dfac4  9237  kmlem6  9271  kmlem8  9273  kmlem9  9274  infpssr  9424  fin1a2lem12  9527  axcc4  9555  axcc4dom  9557  ac6s2  9602  zornn0g  9621  cardidg  9664  unsnen  9669  pwcfsdom  9699  cfpwsdom  9700  gchpwdom  9786  r1tskina  9898  intgru  9930  indpi  10023  nqereu  10045  supsrlem  10226  letrii  10456  dfnn3  11330  zaddcl  11702  nn0ind  11757  fnn0ind  11761  ublbneg  12011  nn01to3  12019  infmrp1  12411  fz0  12598  fzo1fzo0n0  12762  elfzom1elp1fzo  12778  fzo0end  12803  elfznelfzo  12816  fzind2  12829  injresinjlem  12831  fleqceilz  12896  nnsinds  13030  nn0sinds  13031  faclbnd4lem1  13319  hashinf  13361  hasheqf1oi  13379  hashgt0elex  13425  hashfacen  13474  hash2prde  13488  hash2sspr  13506  fun2dmnop0  13512  swrdn0  13673  swrdlsw  13695  swrdswrdlem  13702  swrdccatin12lem3  13733  swrdccat3  13735  swrdccat3blem  13738  cshwsublen  13785  cshwidxmod  13792  repswcshw  13801  cshw1  13811  trclun  13997  dmtrclfv  14001  rediv  14113  imdiv  14120  sqrt0  14224  fsump1i  14742  modfsummods  14766  bpolydiflem  15024  bpoly3  15028  bpoly4  15029  cos1bnd  15156  sinltx  15158  rpnnen2lem1  15182  rpnnen2lem2  15183  rpnnen2lem12  15193  odd2np1  15304  opoe  15326  omoe  15327  opeo  15328  omeo  15329  gcdcllem1  15459  gcdaddmlem  15483  dfgcd2  15501  algfx  15531  lcmledvds  15550  lcmfunsnlem  15592  lcmfun  15596  coprmprod  15612  coprmproddvdslem  15613  odzval  15732  odzdvds  15736  prmreclem5  15860  mul4sq  15894  prmgaplem5  15995  prmgaplem6  15996  imasaddfnlem  16412  mreexexlem4d  16531  joindmss  17231  meetdmss  17245  gictr  17938  cntzval  17974  symg2bas  18038  efgsfo  18372  efgrelexlemb  18383  dprddomcld  18621  dprdsubg  18644  dprd2da  18662  lssacs  19193  cnfldinv  20004  ocvval  20241  dmatmul  20534  mdetfval1  20627  mndifsplit  20673  fvmptnn04if  20887  opnnei  21158  ordtbas2  21229  ordtrest2lem  21241  lmmo  21418  fincmp  21430  bwth  21447  txbas  21604  ptcnplem  21658  tx2ndc  21688  hmphtr  21820  fbun  21877  filconn  21920  ptcmplem5  22093  cnextcn  22104  utoptop  22271  ucncn  22322  metust  22596  cfilucfil  22597  elcncf1di  22931  xrhmeo  22978  phtpycc  23023  copco  23050  pcohtpylem  23051  pcopt  23054  pcopt2  23055  ncvsi  23183  ovolval  23476  iunmbl2  23560  itg2splitlem  23751  cpnfval  23931  plyval  24185  fta1  24299  aaliou2b  24332  tayl0  24352  ulmdvlem3  24392  radcnvlem2  24404  dvradcnv  24411  reeff1o  24437  sincosq1lem  24486  sincosq2sgn  24488  sincosq4sgn  24490  sinq12ge0  24497  logrncl  24550  eflog  24559  cxpge0  24665  logb1  24743  atanf  24843  atanbnd  24889  igamf  25013  igamcl  25014  lgsne0  25296  mul2sq  25380  pntibnd  25518  ostth  25564  mptelee  26011  axlowdimlem9  26066  axlowdimlem12  26069  axcontlem2  26081  axcontlem12  26091  structgrssvtx  26149  structgrssiedg  26150  structgrssvtxOLD  26152  structgrssiedgOLD  26153  lpvtx  26199  nbuhgr  26477  nbumgr  26481  nbuhgr2vtx1edgblem  26485  nbgr0vtxlem  26489  nbgr1vtx  26492  uvtx01vtx  26540  uvtxa01vtx0OLD  26542  prcliscplgr  26559  cusgrsizeinds  26598  sizusglecusglem2  26608  uhgrvd00  26680  fusgrregdegfi  26715  rusgr1vtxlem  26733  wlkeq  26779  wlk1walk  26785  uspgr2wlkeq  26792  wlklenvclwlk  26801  wlkreslem  26816  wlkdlem2  26830  wlkdlem4  26832  spthonepeq  26898  clwlkclwwlkflem  27169  clwlkclwwlkfolem  27172  clwlkclwwlkf  27173  clwwisshclwws  27180  clwwlkneq0  27198  3wlkdlem6  27360  eupth2eucrct  27412  eupth2lem1  27413  eupth2lem3lem7  27429  frgr3vlem1  27470  frgr3vlem2  27471  frgrncvvdeqlem8  27503  frgrncvvdeqlem9  27504  numclwwlk5  27598  frgrreg  27604  frgrregord013  27605  friendshipgt3  27608  isgrpo  27702  vciOLD  27766  vcex  27783  nmogtmnf  27975  siilem1  28056  siii  28058  ajmoi  28064  bcsiALT  28386  hhcms  28410  ocval  28489  hsupval  28543  omlsilem  28611  h1de2bi  28763  h1de2ctlem  28764  hosubeq0i  29035  adjmo  29041  nmopgtmnf  29077  nlfnval  29090  nmcopex  29238  nmcfnex  29262  riesz4i  29272  riesz1  29274  riesz2  29275  opsqrlem1  29349  superpos  29563  hatomistici  29571  chpssati  29572  mdsymlem3  29614  3o1cs  29659  3o2cs  29660  3o3cs  29661  spc2ed  29662  brabgaf  29767  f1mptrn  29784  ffsrn  29853  fpwrelmap  29857  ordtrest2NEWlem  30315  qqhval2  30373  esumfsup  30479  esumcvg  30495  cntnevol  30638  ddemeas  30646  dya2icoseg2  30687  dya2iocnei  30691  eulerpartlems  30769  eulerpartlemgvv  30785  eulerpart  30791  cndprobprob  30847  ballotlemsdom  30920  ballotth  30946  sgn3da  30950  bnj945  31188  bnj1379  31245  bnj1459  31257  bnj557  31315  bnj571  31320  bnj849  31339  bnj964  31357  bnj978  31363  bnj1018  31376  bnj1020  31377  bnj1033  31381  bnj1175  31416  bnj1398  31446  bnj1417  31453  bnj1523  31483  txpconn  31558  msubco  31772  mclsax  31810  setinds  32024  dfon2lem7  32035  dfon2lem8  32036  poseq  32095  soseq  32096  frrlem4  32125  nocvxminlem  32235  nocvxmin  32236  pprodss4v  32333  fullfunfv  32396  altxpsspw  32426  funtransport  32480  fvtransport  32481  funray  32589  fvray  32590  funline  32591  fvline  32593  finminlem  32654  bisym1  32756  onsucconni  32774  onsucsuccmpi  32780  bj-alcomexcom  33006  axc11n11r  33009  bj-equsal2  33143  bj-xpima1snALT  33272  bj-bm1.3ii  33352  mptsnunlem  33520  iooelexlt  33544  relowlpssretop  33546  rdgeqoa  33552  cnfinltrel  33575  wl-lem-nexmo  33681  matunitlindflem1  33736  ptrecube  33740  poimirlem26  33766  poimirlem30  33770  poimir  33773  ismblfin  33781  itg2addnclem  33791  dvasin  33826  sdclem2  33867  totbndbnd  33917  ismgmOLD  33978  exidresid  34007  isrngo  34025  rngoablo2  34037  rngoueqz  34068  isdivrngo  34078  isdrngo1  34084  isdrngo2  34086  ispridl2  34166  relcnveq3  34425  elrelscnveq3  34572  prtlem11  34663  ax12eq  34738  ax12el  34739  lkr0f  34892  hl2at  35203  dalemswapyz  35454  pclfinclN  35748  osumcllem11N  35764  pexmidlem8N  35775  ltrnnid  35934  mptfcl  37802  fphpd  37899  elmnc  38224  itgoval  38249  arearect  38318  clsk3nimkb  38855  nanorxor  39021  pm11.71  39114  iotavalsb  39150  sbiota1  39151  2uasbanh  39292  eel0TT  39444  eelT00  39445  eelTTT  39446  eelT11  39447  eelT12  39449  eelTT1  39450  eelT01  39451  eel0T1  39452  eelTT  39512  uunT1p1  39522  uun121  39524  uun121p1  39525  un2122  39531  uunTT1  39534  uunTT1p1  39535  uunTT1p2  39536  uunT11  39537  uunT11p1  39538  uunT11p2  39539  uunT12  39540  uunT12p1  39541  uunT12p2  39542  uunT12p3  39543  uunT12p4  39544  uunT12p5  39545  uun111  39546  3anidm12p2  39548  uun123  39549  3impdirp1  39557  undif3VD  39629  ax6e2ndeqVD  39656  2uasbanhVD  39658  ax6e2ndeqALT  39678  iunconnlem2  39682  sineq0ALT  39684  ioodvbdlimc1lem2  40644  ioodvbdlimc2lem  40646  stoweidlem3  40716  stoweidlem17  40730  fourierdlem42  40862  fourierdlem48  40867  fourierdlem50  40869  fourierdlem51  40870  fourierdlem76  40895  fourierdlem83  40902  fourierdlem87  40906  hoidmvval0  41300  raaan2  41666  rexrsb  41699  afv0nbfvbi  41757  afvfv0bi  41758  afveu  41759  fnbrafvb  41760  afvres  41778  tz6.12-afv  41779  dmfcoafv  41781  afvco2  41782  aovprc  41794  aovrcl  41795  aovmpt4g  41807  afv2eu  41844  afv2res  41845  tz6.12-afv2  41846  tz6.12i-afv2  41849  afv2rnfveq  41868  fvmptrab  41899  fvmptrabdm  41900  fzopred  41924  2ffzoeq  41930  pfxccat3  42018  pfxccat3a  42021  lighneal  42120  odd2prm2  42219  even3prm2  42220  upgrwlkupwlk  42306  elsprel  42310  ovn0ssdmfun  42352  islinindfis  42823  setrec2fun  43024  elsetrecslem  43030  setrecsres  43033  secval  43076  cscval  43077  cotval  43078
  Copyright terms: Public domain W3C validator