Theorem mpbiri 257

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

Step	Hyp	Ref	Expression
1		mpbiri.min	. . 3 ⊢ 𝜒
2	1	a1i 11	. 2 ⊢ (𝜑 → 𝜒)
3		mpbiri.maj	. 2 ⊢ (𝜑 → (𝜓 ↔ 𝜒))
4	2, 3	mpbird 256	1 ⊢ (𝜑 → 𝜓)

Syntax hints:   → wi 4   ↔ wb 205

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 206

This theorem is referenced by:  elimh  1081  spei  2391  nfald2  2442  nfabd2  2927  raleleqALT  3339  dedhb  3698  sbceqalOLD  3843  csbie2df  4439  ssdifeq0  4485  r19.2zb  4494  dedth  4585  pwidg  4621  elpr2OLD  4653  snidg  4661  rexreusng  4682  exsnrex  4683  ifpr  4694  rmosn  4722  rabrsn  4727  prid1g  4763  tpid1g  4772  tpid2g  4774  tpid3g  4775  pwpw0  4815  sssn  4828  elpreqpr  4866  pwsnOLD  4900  unimax  4947  intmin3  4979  eqbrtrdi  5186  al0ssb  5307  intabs  5341  pwnss  5348  difelpw  5350  rabelpw  5351  0inp0  5356  intidg  5456  copsexgw  5489  copsexg  5490  euotd  5512  elopab  5526  elvvuni  5751  posn  5760  frsn  5762  eqrelriv  5788  relsnb  5801  relopabiALT  5822  opabid2  5827  ididg  5852  iss  6034  dfpo2  6294  ord0eln0  6418  sucidg  6444  nsuceq0  6446  funopg  6581  fn0  6680  f00  6772  f0bi  6773  f10d  6866  f1o00  6867  fo00  6868  brprcneu  6880  brprcneuALT  6881  dffn5  6949  fsn  7134  funop  7148  funsndifnop  7150  fnsnb  7165  eufnfv  7232  f1eqcocnv  7301  f1eqcocnvOLD  7302  nfriotadw  7375  nfriotad  7379  riotaprop  7395  oprabidw  7442  oprabid  7443  elrnmpo  7547  ov6g  7573  ovelrn  7585  caovmo  7646  offn  7685  caofinvl  7702  fr3nr  7761  onprc  7767  ordeleqon  7771  onint0  7781  0elsuc  7825  onuninsuci  7831  orduninsuc  7834  ordzsl  7836  onzsl  7837  tfinds  7851  limomss  7862  limom  7873  peano5  7886  peano5OLD  7887  xpexr  7911  eqop2  8020  opreuopreu  8022  1stconst  8088  2ndconst  8089  frxp2  8132  frxp3  8139  funsssuppss  8177  dftpos3  8231  dftpos4  8232  wfrlem4OLD  8314  wfrlem14OLD  8324  oawordeulem  8556  omwordi  8573  nnmwordi  8637  riiner  8786  ecopover  8817  map0g  8880  mapsnd  8882  elixpsn  8933  en0  9015  en0OLD  9016  en0ALT  9017  en0r  9018  en1  9023  en1OLD  9024  fiprc  9047  sbthlem2  9086  sbthlem4  9088  sbthlem5  9089  0domg  9102  findcard  9165  findcard2  9166  nneneq  9211  nneneqOLD  9223  sdom1  9244  sdom1OLD  9245  1sdom2dom  9249  fineqvlem  9264  nfielex  9275  enp1i  9281  findcard2OLD  9286  elfiun  9427  marypha1lem  9430  oicl  9526  oif  9527  oion  9533  hartogslem1  9539  hartogs  9541  wemapso2  9550  card2on  9551  0wdom  9567  brwdom2  9570  inf3lem6  9630  cantnflem3  9688  cantnflem4  9689  wemapwe  9694  cnfcom  9697  ssttrcl  9712  ttrclselem2  9723  tctr  9737  r1tr  9773  r1rankidb  9801  r1pw  9842  scottex  9882  scott0  9883  bnd2  9890  eldju2ndl  9921  tskwe  9947  oncard  9957  cardlim  9969  harsdom  9992  en2eleq  10005  dfac8alem  10026  cardaleph  10086  iunfictbso  10111  infmap2  10215  ackbij1lem18  10234  cff  10245  cfsuc  10254  cff1  10255  cflim2  10260  cfss  10262  sdom2en01  10299  infpssrlem4  10303  fin23lem7  10313  fin23lem11  10314  isfin2-2  10316  fin23lem26  10322  fin23lem19  10333  fin23lem17  10335  isf34lem2  10370  isf34lem4  10374  fin1a2lem6  10402  fin1a2lem10  10406  fin1a2lem12  10408  itunifn  10414  hsmexlem1  10423  axcc2lem  10433  dcomex  10444  axdc3lem4  10450  ondomon  10560  konigthlem  10565  pwcfsdom  10580  cfpwsdom  10581  axpowndlem3  10596  canth4  10644  canthnumlem  10645  canthwelem  10647  canthwe  10648  canthp1lem2  10650  pwfseqlem4  10659  pwfseqlem5  10660  gchaleph  10668  gch2  10672  winainflem  10690  0tsk  10752  rankcf  10774  tskcard  10778  gruina  10815  grutsk  10819  tskmid  10837  indpi  10904  nqereu  10926  mulcanenq  10957  recmulnq  10961  archnq  10977  ltsopr  11029  1ne0sr  11093  0idsr  11094  00sr  11096  leid  11314  lelttric  11325  divcan3  11902  lemul1a  12072  nn1suc  12238  nn0n0n1ge2b  12544  xnn0xr  12553  xnn0nemnf  12559  nn0lt10b  12628  nn0ind-raph  12666  elnn1uz2  12913  indstr2  12915  uzsupss  12928  rpnnen1lem4  12968  rpnnen1lem5  12969  xrnemnf  13101  xrnepnf  13102  mnfltxr  13111  xnn0n0n1ge2b  13115  xnn0ge0  13117  xrlttri  13122  xrlttr  13123  xrleid  13134  qbtwnxr  13183  xmullem2  13248  xlemul1a  13271  xrub  13295  reltxrnmnf  13325  ixxun  13344  xnn0xrge0  13487  fztpval  13567  fseq1p1m1  13579  elfznelfzob  13742  ltweuz  13930  fzfi  13941  fsuppmapnn0fiubex  13961  ser0f  14025  0exp  14067  faclbnd4lem1  14257  bcn1  14277  hashnemnf  14308  hashv01gt1  14309  hashsnle1  14381  hashgt12el2  14387  hashpw  14400  hashf1  14422  fz1isolem  14426  hash2prb  14437  0wrd0  14494  wrdlen1  14508  ccatvalfn  14535  eqs1  14566  wrdl1exs1  14567  swrdlen  14601  swrdwrdsymb  14616  swrdspsleq  14619  cats1un  14675  wrdind  14676  wrd2ind  14677  swrdccatin1  14679  repswsymballbi  14734  cshw1  14776  scshwfzeqfzo  14781  wrdl2exs2  14901  trclfvcotr  14960  relexp1g  14977  relexp0rel  14988  relexprelg  14989  relexpreld  14991  sqrt0  15192  sqrtsq  15220  mptfzshft  15728  prodf1f  15842  egt2lt3  16153  0dvds  16224  nn0onn  16327  nn0o  16330  divalgmod  16353  flodddiv4  16360  bitsp1o  16378  gcddvds  16448  bezout  16489  lcmdvds  16549  rpdvds  16601  1nprm  16620  prmind2  16626  nnoddn2prmb  16750  pcpre1  16779  vdwapf  16909  vdwapid1  16912  ram0  16959  ramz  16962  prmolefac  16983  cshws0  17039  prmlem0  17043  strle1  17095  restsspw  17381  prdsdsfn  17415  imasdsfn  17464  imasaddfnlem  17478  imasvscafn  17487  xpsfrnel  17512  isacs1i  17605  cidfn  17627  fnhomeqhomf  17639  comffn  17653  isoval  17716  sscres  17774  cofucl  17842  idffth  17888  ressffth  17893  cat1lem  18050  catcoppccl  18071  catcoppcclOLD  18072  estrchomfn  18090  funcestrcsetclem4  18099  funcestrcsetclem7  18102  equivestrcsetc  18108  funcsetcestrclem4  18114  funcsetcestrclem7  18117  1stfcl  18153  2ndfcl  18154  prfcl  18159  evlfcl  18179  curf1cl  18185  curfcl  18189  hofcl  18216  yonedainv  18238  pospo  18302  lubfun  18309  glbfun  18322  joindmss  18336  meetdmss  18350  ipopos  18493  acsficl2d  18509  dirref  18558  mgmidcl  18591  mgmlrid  18592  ielefmnd  18804  smndex1basss  18822  smndex1n0mnd  18829  cntzssv  19233  idresperm  19294  symgvalstruct  19305  symgvalstructOLD  19306  pmtrfmvdn0  19371  symggen  19379  psgnunilem1  19402  psgnprfval  19430  slwpgp  19522  frgpmhm  19674  frgpuptinv  19680  frgpup3lem  19686  gsumzoppg  19853  gsumcom2  19884  c0snmhm  20354  abv0  20582  rrgsupp  21107  zrhrhm  21280  psgnodpmr  21362  frlmphllem  21554  ellspd  21576  psrvscafval  21728  psrridm  21743  ltbwe  21818  psrbag0  21842  psrbagsn  21843  subrgascl  21846  mattpostpos  22176  mavmul0  22274  mavmul0g  22275  mdet0f1o  22315  m1detdiag  22319  m2detleiblem5  22347  m2detleiblem6  22348  m2detleiblem3  22351  m2detleiblem4  22352  maducoeval2  22362  d1mat2pmat  22461  chpmat1dlem  22557  chpmat1d  22558  baspartn  22677  eltg3  22685  topnex  22719  fctop  22727  cctop  22729  discld  22813  mretopd  22816  neipeltop  22853  neitr  22904  restcls  22905  ordtbaslem  22912  ordtuni  22914  idcn  22981  cnrmi  23084  cmpsublem  23123  cmpsub  23124  tgcmp  23125  uncmp  23127  hauscmplem  23130  cmpfi  23132  bwth  23134  1stcrestlem  23176  disllycmp  23222  dis1stc  23223  refref  23237  kgeni  23261  1stckgenlem  23277  kqffn  23449  snfil  23588  filconn  23607  cfinfil  23617  ufileu  23643  filufint  23644  fixufil  23646  cfinufil  23652  ufilen  23654  fin1aufil  23656  fmf  23669  rnelfm  23677  flimclslem  23708  hauspwpwf1  23711  supnfcls  23744  flimfnfcls  23752  fclscmp  23754  alexsubALTlem2  23772  alexsubALTlem3  23773  alexsubALT  23775  ptcmplem1  23776  cnextrel  23787  tsmsfbas  23852  ustref  23943  trust  23954  restutop  23962  isusp  23986  xmet0  24068  imasdsf1olem  24099  blfvalps  24109  blfps  24132  blf  24133  restmetu  24299  dscmet  24301  isngp2  24326  nm0  24358  nrginvrcn  24429  nmoix  24466  qdensere  24506  iccconn  24566  iccpnfcnv  24689  xrhmeo  24691  lebnumlem3  24709  metsscmetcld  25063  bcthlem5  25076  csschl  25124  rrxmfval  25154  minveclem3b  25176  cniccbdd  25210  ovolicc2lem4  25269  iunmbl  25302  ioorinv  25325  ioorcl  25326  i1f1lem  25438  limcvallem  25620  ellimc2  25626  limccnp  25640  limccnp2  25641  limcco  25642  perfdvf  25652  recnprss  25653  fncpn  25683  dvcmulf  25696  c1lip1  25749  lhop2  25767  q1pcl  25908  r1pdeglt  25911  ply1remlem  25915  plyssc  25949  ulm0  26139  cxpeq0  26422  cxplea  26440  cxplogb  26527  asinlem  26609  isppw2  26855  muval2  26874  dchrfi  26994  dchrpt  27006  bposlem6  27028  lgsdir2lem2  27065  lgsqr  27090  gausslemma2dlem4  27108  2lgslem2  27134  2lgslem3  27143  2lgs  27146  2sqlem7  27163  2sqlem11  27168  chtppilim  27214  nosgnn0i  27398  nolesgn2ores  27411  nogesgn1ores  27413  nosepnelem  27418  nosepdmlem  27422  nosupbnd1lem3  27449  nosupbnd1lem5  27451  nosupbnd2lem1  27454  noinfbnd1lem3  27464  noinfbnd1lem5  27466  noinfbnd2lem1  27469  oldval  27586  made0  27605  lrrecpo  27663  n0scut  27943  tgldimor  28020  tgcgr4  28049  tglnfn  28065  tglnunirn  28066  mirne  28185  mircinv  28186  perpln1  28228  perpln2  28229  lmiisolem  28314  xmstrkgc  28410  axcgrtr  28440  axsegconlem9  28450  axlowdimlem5  28471  axlowdimlem17  28483  axlowdim1  28484  uhgr0e  28598  edglnl  28670  uhgr0edgfi  28764  issubgr2  28796  subgrprop2  28798  egrsubgr  28801  0grsubgr  28802  0uhgrsubgr  28803  uhgrsubgrself  28804  nbgr0vtx  28880  nbgr1vtx  28882  nbgrssovtx  28885  nb3grprlem1  28904  uvtx01vtx  28921  cplgr1vlem  28953  cplgr1v  28954  usgrexilem  28964  wlkcomp  29155  wlk1walk  29163  wlkp1lem5  29201  uhgrwkspthlem1  29277  pthdlem1  29290  clwlkcomp  29303  lfgrn1cycl  29326  uspgrn2crct  29329  wwlksn0s  29382  umgrwwlks2on  29478  clwwlkn  29546  clwwlkn1  29561  0ewlk  29634  1ewlk  29635  0spth  29646  upgr1wlkdlem2  29666  wlk2v2e  29677  upgr3v3e3cycl  29700  upgr4cycl4dv4e  29705  eupth0  29734  frgr0v  29782  frgr1v  29791  1vwmgr  29796  ex-opab  29952  grpoinvf  30052  nvmid  30179  nmlnoubi  30316  hiidrcl  30615  hsn0elch  30768  shjshseli  31013  cmbr4i  31121  dfiop2  31273  kbpj  31476  nmopun  31534  adjeq0  31611  kbass2  31637  pjssdif1i  31695  pjinvari  31711  pjcmul2i  31722  pj3i  31728  stge1i  31758  stle0i  31759  sumdmdlem2  31939  dmdbr6ati  31943  dmdbr7ati  31944  rabsnel  32007  unidifsnel  32039  unidifsnne  32040  disjdifprg  32073  ofoprabco  32156  padct  32211  fpwrelmapffslem  32224  xrlelttric  32232  xnn0gt0  32249  iundisj2cnt  32277  f1ocnt  32280  fz1nnct  32281  fz1nntr  32282  hashxpe  32286  dvdszzq  32288  nn0min  32293  wrdt2ind  32384  xrge0tsmsbi  32480  opprabs  32870  locfinref  33119  dispcmp  33137  zartopn  33153  zarcmplem  33159  pstmxmet  33175  xrge0iifcnv  33211  xrge0iif1  33216  qqhre  33298  esumcl  33326  esumpr2  33363  esumpinfval  33369  esumpcvgval  33374  ofcfn  33396  pwsiga  33426  prsiga  33427  sigainb  33432  ldgenpisyslem1  33459  measiuns  33513  relfae  33543  pmeasmono  33621  sitgf  33644  eulerpartgbij  33669  sgnmulsgn  33846  sgnmulsgp  33847  signswch  33870  signslema  33871  signstlen  33876  signstfvn  33878  circlevma  33952  bnj216  34041  bnj151  34186  bnj517  34194  bnj970  34256  bnj1145  34302  bnj1498  34370  fineqvrep  34393  fineqvac  34395  0nn0m1nnn0  34400  pthhashvtx  34416  acycgr0v  34437  prclisacycgr  34440  umgracycusgr  34443  cusgracyclt3v  34445  subfacp1lem5  34473  erdszelem8  34487  kur14lem1  34495  indispconn  34523  cvmsss2  34563  satfvsuclem2  34649  satfrel  34656  satfrnmapom  34659  satfv0fun  34660  satf00  34663  satf0suclem  34664  fmlasuc0  34673  msubrn  34818  dfon2lem7  35065  brbigcup  35174  elsingles  35194  fnimage  35205  funpartlem  35218  dfrdg4  35227  imagesset  35229  altopthsn  35237  elaltxp  35251  ellines  35428  linethru  35429  rankeq1o  35447  elhf2  35451  hfninf  35462  nn0prpwlem  35510  fneref  35538  neibastop2lem  35548  limsucncmpi  35633  bj-exlimmpbir  36097  curryset  36130  bj-snglex  36157  bj-restpw  36276  bj-inftyexpidisj  36394  topdifinffinlem  36531  relowlssretop  36547  rdgeqoa  36554  finxpreclem6  36580  fvineqsneq  36596  pibt2  36601  poimirlem23  36814  poimirlem29  36820  poimirlem31  36822  volsupnfl  36836  cnambfre  36839  dvasin  36875  dvacos  36876  sdclem2  36913  sstotbnd2  36945  ssbnd  36959  ismgmOLD  37021  grpokerinj  37064  rngomndo  37106  isdrngo1  37127  ac6s6  37343  iss2  37516  cnvelrels  37668  cosselrels  37669  brssrid  37675  brcnvssrid  37680  dfdisjs5  37885  eldisjs5  37899  mpets2  38014  pets  38025  prtlem12  38040  riotasv2d  38130  lkrscss  38271  islshpkrN  38293  isline  38913  ispointN  38916  0psubN  38923  linepsubN  38926  atpsubN  38927  cdlemk36  40087  diafn  40208  dibfna  40328  dibvalrel  40337  dicvalrelN  40359  diclspsn  40368  dihvalrel  40453  dih1  40460  lclkrlem1  40680  lclkr  40707  mapd1o  40822  mapdin  40836  hdmapfnN  41003  hgmapfnN  41062  lcmineqlem10  41209  sticksstones9  41276  sn-iotalem  41344  repncan2  41557  sn-inelr  41640  elrfirn  41735  ismrcd1  41738  istopclsd  41740  rabren3dioph  41855  jm2.17b  42002  jm2.22  42036  jm2.23  42037  ttac  42077  pw2f1ocnv  42078  dnnumch1  42088  hbtlem5  42172  mncn0  42183  aaitgo  42206  rngunsnply  42217  unielss  42269  onexlimgt  42294  cantnfresb  42376  dflim5  42381  naddwordnexlem4  42454  safesnsupfiss  42468  safesnsupfidom1o  42470  safesnsupfilb  42471  ensucne0OLD  42583  clcnvlem  42676  relexp01min  42766  ntrf  43176  ssrecnpr  43369  seff  43370  sblpnf  43371  nzss  43378  dvconstbi  43395  ipo0  43510  ifr0  43511  addrfn  43533  subrfn  43534  mulvfn  43535  refsum2cnlem1  44023  rn1st  44276  ellimciota  44628  dvmptconst  44929  dvmptidg  44931  dvmulcncf  44939  dvdivcncf  44941  stoweidlem26  45040  stoweidlem50  45064  stoweidlem57  45071  aiotaval  46101  ndfatafv2nrn  46227  afv2ndefb  46230  funop1  46289  fun2dmnopgexmpl  46290  2ffzoeq  46334  iccpartiltu  46388  iccpartigtl  46389  zofldiv2ALTV  46628  evenprm2  46680  9fppr8  46703  stgoldbwt  46742  nnsum3primesle9  46760  nnsum4primeseven  46766  nnsum4primesevenALTV  46767  tgblthelfgott  46781  isomgreqve  46791  uspgrex  46826  0mgm  46842  nnsgrpmgm  46852  rngchomffvalALTV  46981  funcringcsetcALTV2lem4  47025  funcringcsetclem4ALTV  47048  srhmsubc  47062  rhmsubclem1  47072  srhmsubcALTV  47080  rhmsubcALTVlem1  47090  mapsnop  47108  zlmodzxzldeplem4  47271  zofldiv2  47304  fdivval  47312  nnlog2ge0lt1  47339  dig1  47381  itcoval2  47437  itcoval3  47438  mosn  47584  mo0  47585  mof02  47592  mofeu  47601  f102g  47605  f1mo  47606  f1omo  47614  intubeu  47696  unilbeu  47697  functhinclem1  47748  fullthinc  47753  thincciso  47756  indthinc  47759  indthincALT  47760