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

Theorem mpbiri 259
Description: An inference from a nested biconditional, related to modus ponens. (Contributed by NM, 21-Jun-1993.) (Proof shortened by Wolf Lammen, 25-Oct-2012.)
Hypotheses
Ref Expression
mpbiri.min 𝜒
mpbiri.maj (𝜑 → (𝜓𝜒))
Assertion
Ref Expression
mpbiri (𝜑𝜓)

Proof of Theorem mpbiri
StepHypRef Expression
1 mpbiri.min . . 3 𝜒
21a1i 11 . 2 (𝜑𝜒)
3 mpbiri.maj . 2 (𝜑 → (𝜓𝜒))
42, 3mpbird 258 1 (𝜑𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 207
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 208
This theorem is referenced by:  elimh  1072  dedtOLD  1075  spei  2403  nfald2  2459  nfabd2  2999  nfabd2OLD  3000  raleleqALT  3426  dedhb  3692  sbceqal  3832  ssdifeq0  4428  r19.2zb  4437  dedth  4519  pwidg  4552  elpr2  4581  snidg  4589  rexreusng  4609  exsnrex  4610  ifpr  4621  rmosn  4647  rabrsn  4652  prid1g  4688  tpid1g  4697  tpid2g  4699  tpid3g  4700  pwpw0  4738  sssn  4751  elpreqpr  4789  pwsnALT  4823  unimax  4865  intmin3  4895  eqbrtrdi  5096  al0ssb  5203  intabs  5236  pwnss  5241  difelpw  5243  rabelpw  5244  0inp0  5250  copsexgw  5372  copsexg  5373  euotd  5394  elopab  5405  epelgOLD  5460  elvvuni  5621  posn  5630  frsn  5632  eqrelriv  5655  relsnb  5668  relopabiALT  5688  opabid2  5693  ididg  5717  iss  5896  ord0eln0  6238  sucidg  6262  nsuceq0  6264  onun2i  6299  funopg  6382  fn0  6472  f00  6554  f0bi  6555  f10d  6641  f1o00  6642  fo00  6643  brprcneu  6655  dffn5  6717  fsn  6889  funop  6903  funsndifnop  6905  fnsnb  6920  eufnfv  6982  f1eqcocnv  7048  nfriotadw  7111  nfriotad  7114  riotaprop  7130  oprabidw  7176  oprabid  7177  elrnmpo  7276  ov6g  7301  ovelrn  7313  caovmo  7374  offn  7409  caofinvl  7425  fr3nr  7483  onprc  7488  ordeleqon  7492  onint0  7500  0elsuc  7539  onuninsuci  7544  orduninsuc  7547  ordzsl  7549  onzsl  7550  tfinds  7563  limomss  7574  limom  7584  peano5  7594  xpexr  7612  eqop2  7721  opreuopreu  7723  1stconst  7784  2ndconst  7785  funsssuppss  7845  dftpos3  7899  dftpos4  7900  wfrlem4  7947  wfrlem14  7957  oawordeulem  8169  omwordi  8186  nnmwordi  8250  riiner  8359  ecopover  8390  map0g  8437  mapsnd  8438  elixpsn  8489  en0  8560  en1  8564  fiprc  8583  sbthlem2  8616  sbthlem4  8618  sbthlem5  8619  nneneq  8688  sdom1  8706  fineqvlem  8720  nfielex  8735  findcard  8745  findcard2  8746  elfiun  8882  marypha1lem  8885  oicl  8981  oif  8982  oion  8988  hartogslem1  8994  hartogs  8996  wemapso2  9005  card2on  9006  0wdom  9022  brwdom2  9025  inf3lem6  9084  cantnflem3  9142  cantnflem4  9143  wemapwe  9148  cnfcom  9151  tctr  9170  r1tr  9193  r1rankidb  9221  r1pw  9262  scottex  9302  scott0  9303  bnd2  9310  eldju2ndl  9341  tskwe  9367  oncard  9377  cardlim  9389  harsdom  9412  en2eleq  9422  dfac8alem  9443  cardaleph  9503  iunfictbso  9528  infmap2  9628  ackbij1lem18  9647  cff  9658  cfsuc  9667  cff1  9668  cflim2  9673  cfss  9675  sdom2en01  9712  infpssrlem4  9716  fin23lem7  9726  fin23lem11  9727  isfin2-2  9729  fin23lem26  9735  fin23lem19  9746  fin23lem17  9748  isf34lem2  9783  isf34lem4  9787  fin1a2lem6  9815  fin1a2lem10  9819  fin1a2lem12  9821  itunifn  9827  hsmexlem1  9836  axcc2lem  9846  dcomex  9857  axdc3lem4  9863  ondomon  9973  konigthlem  9978  pwcfsdom  9993  cfpwsdom  9994  axpowndlem3  10009  canth4  10057  canthnumlem  10058  canthwelem  10060  canthwe  10061  canthp1lem2  10063  pwfseqlem4  10072  pwfseqlem5  10073  gchaleph  10081  gch2  10085  winainflem  10103  0tsk  10165  rankcf  10187  tskcard  10191  gruina  10228  grutsk  10232  tskmid  10250  indpi  10317  nqereu  10339  mulcanenq  10370  recmulnq  10374  archnq  10390  ltsopr  10442  1ne0sr  10506  0idsr  10507  00sr  10509  leid  10724  lelttric  10735  divcan3  11312  lemul1a  11482  nn1suc  11647  nn0n0n1ge2b  11951  xnn0xr  11960  xnn0nemnf  11966  nn0lt10b  12032  nn0ind-raph  12070  elnn1uz2  12313  indstr2  12315  uzsupss  12328  rpnnen1lem4  12367  rpnnen1lem5  12368  xrnemnf  12500  xrnepnf  12501  mnfltxr  12510  xnn0n0n1ge2b  12514  xnn0ge0  12516  xrlttri  12520  xrlttr  12521  xrleid  12532  qbtwnxr  12581  xmullem2  12646  xlemul1a  12669  xrub  12693  reltxrnmnf  12723  ixxun  12742  xnn0xrge0  12879  fztpval  12957  fseq1p1m1  12969  elfznelfzob  13131  ltweuz  13317  fzfi  13328  fsuppmapnn0fiubex  13348  ser0f  13411  0exp  13452  faclbnd4lem1  13641  bcn1  13661  hashnemnf  13692  hashv01gt1  13693  hashsnle1  13766  hashgt12el2  13772  hashpw  13785  hashf1  13803  fz1isolem  13807  hash2prb  13818  wrdlndmOLD  13868  0wrd0  13878  wrdlen1  13894  ccatvalfn  13923  eqs1  13954  wrdl1exs1  13955  swrdlen  13997  swrdwrdsymb  14012  swrdspsleq  14015  cats1un  14071  wrdind  14072  wrd2ind  14073  swrdccatin1  14075  repswsymballbi  14130  cshw1  14172  scshwfzeqfzo  14176  wrdl2exs2  14296  trclfvcotr  14357  relexp1g  14373  relexp0rel  14384  relexprelg  14385  sqr0lem  14588  sqrtsq  14617  mptfzshft  15121  prodf1f  15236  fprodrev  15319  egt2lt3  15547  0dvds  15618  nn0onn  15719  nn0o  15722  divalgmod  15745  flodddiv4  15752  bitsp1o  15770  gcddvds  15840  bezout  15879  lcmdvds  15940  rpdvds  15992  1nprm  16011  prmind2  16017  nnoddn2prmb  16138  pcpre1  16167  vdwapf  16296  vdwapid1  16299  ram0  16346  ramz  16349  prmolefac  16370  cshws0  16423  prmlem0  16427  strle1  16580  restsspw  16693  prdsdsfn  16726  imasdsfn  16775  imasaddfnlem  16789  imasvscafn  16798  xpsfrnel  16823  isacs1i  16916  cidfn  16938  fnhomeqhomf  16949  comffn  16963  isoval  17023  sscres  17081  cofucl  17146  idffth  17191  ressffth  17196  catcoppccl  17356  estrchomfn  17373  funcestrcsetclem4  17381  funcestrcsetclem7  17384  equivestrcsetc  17390  funcsetcestrclem4  17396  funcsetcestrclem7  17399  1stfcl  17435  2ndfcl  17436  prfcl  17441  evlfcl  17460  curf1cl  17466  curfcl  17470  hofcl  17497  yonedainv  17519  pospo  17571  lubfun  17578  glbfun  17591  joindmss  17605  meetdmss  17619  ipopos  17758  acsficl2d  17774  dirref  17833  mgmidcl  17864  mgmlrid  17865  cntzssv  18396  idresperm  18448  symgid  18459  pmtrfmvdn0  18519  symggen  18527  psgnunilem1  18550  psgnprfval  18578  slwpgp  18667  frgpmhm  18820  frgpuptinv  18826  frgpup3lem  18832  gsumzoppg  18993  gsumcom2  19024  abv0  19531  rrgsupp  19992  psrvscafval  20098  psrridm  20112  ltbwe  20181  psrbag0  20202  psrbagsn  20203  subrgascl  20206  zrhrhm  20587  psgnodpmr  20662  frlmphllem  20852  frlmphl  20853  ellspd  20874  mattpostpos  20991  mavmul0  21089  mavmul0g  21090  mdet0f1o  21130  m1detdiag  21134  m2detleiblem5  21162  m2detleiblem6  21163  m2detleiblem3  21166  m2detleiblem4  21167  maducoeval2  21177  d1mat2pmat  21275  chpmat1dlem  21371  chpmat1d  21372  baspartn  21490  eltg3  21498  topnex  21532  fctop  21540  cctop  21542  discld  21625  mretopd  21628  neipeltop  21665  neitr  21716  restcls  21717  ordtbaslem  21724  ordtuni  21726  idcn  21793  cnrmi  21896  cmpsublem  21935  cmpsub  21936  tgcmp  21937  uncmp  21939  hauscmplem  21942  cmpfi  21944  bwth  21946  1stcrestlem  21988  disllycmp  22034  dis1stc  22035  refref  22049  kgeni  22073  1stckgenlem  22089  kqffn  22261  snfil  22400  filconn  22419  cfinfil  22429  ufileu  22455  filufint  22456  fixufil  22458  cfinufil  22464  ufilen  22466  fin1aufil  22468  fmf  22481  rnelfm  22489  flimclslem  22520  hauspwpwf1  22523  supnfcls  22556  flimfnfcls  22564  fclscmp  22566  alexsubALTlem2  22584  alexsubALTlem3  22585  alexsubALT  22587  ptcmplem1  22588  cnextrel  22599  tsmsfbas  22663  ustref  22754  trust  22765  restutop  22773  isusp  22797  xmet0  22879  imasdsf1olem  22910  blfvalps  22920  blfps  22943  blf  22944  restmetu  23107  dscmet  23109  isngp2  23133  nm0  23165  nrginvrcn  23228  nmoix  23265  qdensere  23305  iccconn  23365  iccpnfcnv  23475  xrhmeo  23477  lebnumlem3  23494  metsscmetcld  23845  bcthlem5  23858  csschl  23906  rrxmfval  23936  minveclem3b  23958  cniccbdd  23989  ovolicc2lem4  24048  iunmbl  24081  ioorinv  24104  ioorcl  24105  i1f1lem  24217  limcvallem  24396  ellimc2  24402  limccnp  24416  limccnp2  24417  limcco  24418  perfdvf  24428  recnprss  24429  fncpn  24457  dvcmulf  24469  c1lip1  24521  lhop2  24539  q1pcl  24676  r1pdeglt  24679  ply1remlem  24683  plyssc  24717  ulm0  24906  cxpeq0  25188  cxplea  25206  cxplogb  25291  asinlem  25373  isppw2  25619  muval2  25638  dchrfi  25758  dchrpt  25770  bposlem6  25792  lgsdir2lem2  25829  lgsqr  25854  gausslemma2dlem4  25872  2lgslem2  25898  2lgslem3  25907  2lgs  25910  2sqlem7  25927  2sqlem11  25932  chtppilim  25978  tgldimor  26215  tgcgr4  26244  tglnfn  26260  tglnunirn  26261  mirne  26380  mircinv  26381  perpln1  26423  perpln2  26424  lmiisolem  26509  xmstrkgc  26599  axcgrtr  26628  axsegconlem9  26638  axlowdimlem5  26659  axlowdimlem17  26671  axlowdim1  26672  uhgr0e  26783  edglnl  26855  uhgr0edgfi  26949  issubgr2  26981  subgrprop2  26983  egrsubgr  26986  0grsubgr  26987  0uhgrsubgr  26988  uhgrsubgrself  26989  nbgr0vtx  27065  nbgr1vtx  27067  nbgrssovtx  27070  nb3grprlem1  27089  uvtx01vtx  27106  cplgr1vlem  27138  cplgr1v  27139  usgrexilem  27149  wlkcomp  27339  wlk1walk  27347  wlkp1lem5  27386  uhgrwkspthlem1  27461  pthdlem1  27474  clwlkcomp  27487  lfgrn1cycl  27510  uspgrn2crct  27513  wwlksn0s  27566  umgrwwlks2on  27663  clwwlkn  27731  clwwlkn1  27746  0ewlk  27820  1ewlk  27821  0spth  27832  upgr1wlkdlem2  27852  wlk2v2e  27863  upgr3v3e3cycl  27886  upgr4cycl4dv4e  27891  eupth0  27920  frgr0v  27968  frgr1v  27977  1vwmgr  27982  ex-opab  28138  grpoinvf  28236  nvmid  28363  nmlnoubi  28500  hiidrcl  28799  hsn0elch  28952  shjshseli  29197  cmbr4i  29305  dfiop2  29457  kbpj  29660  nmopun  29718  adjeq0  29795  kbass2  29821  pjssdif1i  29879  pjinvari  29895  pjcmul2i  29906  pj3i  29912  stge1i  29942  stle0i  29943  sumdmdlem2  30123  dmdbr6ati  30127  dmdbr7ati  30128  rabsnel  30190  unidifsnel  30222  unidifsnne  30223  disjdifprg  30253  ofoprabco  30337  padct  30381  fpwrelmapffslem  30394  xrlelttric  30402  xnn0gt0  30420  iundisj2cnt  30448  f1ocnt  30451  fz1nnct  30452  fz1nntr  30453  hashxpe  30455  dvdszzq  30457  nn0min  30463  wrdt2ind  30554  xrge0tsmsbi  30620  locfinref  31004  dispcmp  31022  pstmxmet  31036  xrge0iifcnv  31075  xrge0iif1  31080  qqhre  31160  esumcl  31188  esumpr2  31225  esumpinfval  31231  esumpcvgval  31236  ofcfn  31258  pwsiga  31288  prsiga  31289  sigainb  31294  ldgenpisyslem1  31321  measiuns  31375  relfae  31405  pmeasmono  31481  sitgf  31504  eulerpartgbij  31529  sgnmulsgn  31706  sgnmulsgp  31707  signswch  31730  signslema  31731  signstlen  31736  signstfvn  31738  circlevma  31812  bnj216  31901  bnj151  32048  bnj517  32056  bnj970  32118  bnj1145  32162  bnj1498  32230  0nn0m1nnn0  32248  pthhashvtx  32271  acycgr0v  32292  prclisacycgr  32295  umgracycusgr  32298  cusgracyclt3v  32300  subfacp1lem5  32328  erdszelem8  32342  kur14lem1  32350  indispconn  32378  cvmsss2  32418  satfvsuclem2  32504  satfrel  32511  satfrnmapom  32514  satfv0fun  32515  satf00  32518  satf0suclem  32519  fmlasuc0  32528  msubrn  32673  dfpo2  32888  dfon2lem7  32931  nosgnn0i  33063  nolesgn2ores  33076  nosepnelem  33081  nosepdmlem  33084  nosupbnd1lem3  33107  nosupbnd1lem5  33109  nosupbnd2lem1  33112  brbigcup  33256  elsingles  33276  fnimage  33287  funpartlem  33300  dfrdg4  33309  imagesset  33311  altopthsn  33319  elaltxp  33333  ellines  33510  linethru  33511  rankeq1o  33529  elhf2  33533  hfninf  33544  nn0prpwlem  33567  fneref  33595  neibastop2lem  33605  limsucncmpi  33690  bj-exlimmpbir  34127  curryset  34154  bj-snglex  34182  bj-restpw  34277  bj-inftyexpidisj  34384  topdifinffinlem  34510  relowlssretop  34526  rdgeqoa  34533  finxpreclem6  34559  fvineqsneq  34575  pibt2  34580  poimirlem23  34796  poimirlem29  34802  poimirlem31  34804  volsupnfl  34818  cnambfre  34821  dvasin  34859  dvacos  34860  sdclem2  34898  sstotbnd2  34933  ssbnd  34947  ismgmOLD  35009  grpokerinj  35052  rngomndo  35094  isdrngo1  35115  ac6s6  35331  iss2  35482  cnvelrels  35615  cosselrels  35616  brssrid  35622  brcnvssrid  35627  dfdisjs5  35825  eldisjs5  35839  prtlem12  35883  riotasv2d  35973  lkrscss  36114  islshpkrN  36136  isline  36755  ispointN  36758  0psubN  36765  linepsubN  36768  atpsubN  36769  cdlemk36  37929  diafn  38050  dibfna  38170  dibvalrel  38179  dicvalrelN  38201  diclspsn  38210  dihvalrel  38295  dih1  38302  lclkrlem1  38522  lclkr  38549  mapd1o  38664  mapdin  38678  hdmapfnN  38845  hgmapfnN  38904  repncan2  39090  elrfirn  39170  ismrcd1  39173  istopclsd  39175  rabren3dioph  39290  jm2.17b  39436  jm2.22  39470  jm2.23  39471  ttac  39511  pw2f1ocnv  39512  dnnumch1  39522  hbtlem5  39606  mncn0  39617  aaitgo  39640  rngunsnply  39651  ensucne0OLD  39774  clcnvlem  39861  relexp01min  39936  ntrf  40351  ssrecnpr  40517  seff  40518  sblpnf  40519  nzss  40526  dvconstbi  40543  ipo0  40658  ifr0  40659  addrfn  40681  subrfn  40682  mulvfn  40683  refsum2cnlem1  41171  ellimciota  41771  dvmptconst  42075  dvmptidg  42077  dvmulcncf  42086  dvdivcncf  42088  stoweidlem26  42188  stoweidlem50  42212  stoweidlem57  42219  aiotaval  43170  ndfatafv2nrn  43297  afv2ndefb  43300  funop1  43359  fun2dmnopgexmpl  43360  2ffzoeq  43405  iccpartiltu  43459  iccpartigtl  43460  zofldiv2ALTV  43704  evenprm2  43756  9fppr8  43779  stgoldbwt  43818  nnsum3primesle9  43836  nnsum4primeseven  43842  nnsum4primesevenALTV  43843  tgblthelfgott  43857  isomgreqve  43867  uspgrex  43902  0mgm  43918  nnsgrpmgm  43960  ielefmnd  43984  smndex1basss  44005  smndex1n0mnd  44012  c0snmhm  44114  rngchomffvalALTV  44194  funcringcsetcALTV2lem4  44238  funcringcsetclem4ALTV  44261  srhmsubc  44275  rhmsubclem1  44285  srhmsubcALTV  44293  rhmsubcALTVlem1  44303  mapsnop  44321  zlmodzxzldeplem4  44486  zofldiv2  44519  fdivval  44527  nnlog2ge0lt1  44554  dig1  44596
  Copyright terms: Public domain W3C validator