Theorem mpbiri 261

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 260	1 ⊢ (𝜑 → 𝜓)

This proof depends on syntax axioms:   → wi 4   ↔ wb 209

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210

This theorem is used by:  elimh  1098  spei  2425  nfald2  2476  nfabd2  2947  raleleq  3334  ceqsexv2d  3503  dedhb  3665  csbie2df  4407  ssdifeq0  4446  dedth  4545  pwidgOLD  4582  snidg  4625  rexreusng  4644  exsnrex  4645  ifpr  4658  rmosn  4684  rabrsn  4689  prid1g  4725  tpid1g  4734  tpid2g  4736  tpid3g  4737  pwpw0  4778  sssn  4791  elpreqpr  4831  unimax  4909  intmin3  4940  eqbrtrdi  5149  al0ssb  5270  vneqv  5278  rabelpw  5306  intabs  5318  difelpw  5323  0inp0  5328  axpr  5397  intidg  5437  copsexgw  5471  copsexgwOLD  5472  copsexg  5473  euotd  5495  elopab  5510  elvvuni  5737  posn  5746  frsn  5748  eqrelriv  5774  relsnb  5788  relopabiALT  5809  opabid2  5814  ididg  5838  iss  6036  dfpo2  6297  ord0eln0  6417  sucidg  6444  nsuceq0  6446  funopg  6570  fn0  6666  f00  6760  f0bi  6761  f10d  6855  f1o00  6856  fo00  6857  brprcneu  6871  brprcneuALT  6872  dffn5  6939  fsn  7131  funop  7146  funsndifnop  7148  fnsnbOLD  7164  eufnfv  7227  f1ounsn  7270  f1eqcocnv  7299  nfriotadw  7377  nfriotad  7380  riotaprop  7396  oprabidw  7443  oprabid  7444  elrnmpo  7548  ov6g  7576  ovelrn  7588  caovmo  7649  offn  7689  caofinvl  7708  fr3nr  7769  onprc  7775  ordeleqon  7779  onint0  7788  0elsuc  7829  onuninsuci  7834  orduninsuc  7837  ordzsl  7839  onzsl  7840  tfinds  7854  limomss  7865  limom  7876  peano5  7888  xpexr  7913  eqop2  8027  opreuopreu  8029  1stconst  8093  2ndconst  8094  frxp2  8138  frxp3  8145  funsssuppss  8184  dftpos3  8238  dftpos4  8239  oawordeulem  8537  omwordi  8554  nnmwordi  8619  riiner  8786  ecopover  8817  map0g  8880  mapsnd  8882  elixpsn  8933  en0  9013  en0ALT  9014  en0r  9015  en1  9019  snfi  9038  fiprc  9039  sbthlem2  9074  sbthlem4  9076  sbthlem5  9077  0domg  9090  findcard  9146  findcard2  9147  nneneq  9188  sdom1  9208  1sdom2dom  9212  fineqvlem  9224  nfielex  9232  enp1i  9237  elfiun  9388  marypha1lem  9391  oicl  9489  oif  9490  oion  9496  hartogslem1  9502  hartogs  9504  wemapso2  9513  card2on  9514  0wdom  9530  brwdom2  9533  elirrv  9557  inf3lem6  9600  cantnflem3  9658  cantnflem4  9659  wemapwe  9664  cnfcom  9667  ssttrcl  9682  ttrclselem2  9693  tctr  9705  r1tr  9746  r1rankidb  9774  r1pw  9815  scottex  9860  scottexOLD  9861  scott0b  9864  scott0OLD  9865  bnd2  9883  eldju2ndl  9917  tskwe  9943  oncard  9953  cardlim  9965  harsdom  9988  en2eleq  9999  dfac8alem  10020  dfac8b  10022  cardaleph  10080  iunfictbso  10105  infmap2  10207  ackbij1lem18  10226  cff  10237  cfsuc  10247  cff1  10248  cflim2  10253  cfss  10255  sdom2en01  10292  infpssrlem4  10296  fin23lem7  10306  fin23lem11  10307  isfin2-2  10309  fin23lem26  10315  fin23lem19  10326  fin23lem17  10328  isf34lem2  10363  isf34lem4  10367  fin1a2lem6  10395  fin1a2lem10  10399  fin1a2lem12  10401  itunifn  10407  hsmexlem1  10416  axcc2lem  10426  dcomex  10437  axdc3lem4  10443  ondomon  10553  konigthlem  10559  pwcfsdom  10574  cfpwsdom  10575  axpowndlem3  10590  canth4  10638  canthnumlem  10639  canthwelem  10641  canthwe  10642  canthp1lem2  10644  pwfseqlem4  10653  pwfseqlem5  10654  gchaleph  10662  gch2  10666  winainflem  10684  0tsk  10746  rankcf  10768  tskcard  10772  gruina  10809  grutsk  10813  tskmid  10831  indpi  10898  nqereu  10920  mulcanenq  10951  recmulnq  10955  archnq  10971  ltsopr  11023  1ne0sr  11087  0idsr  11088  00sr  11090  leid  11312  lelttric  11323  divcan3  11904  divid  11908  div0  11909  lemul1a  12075  nn1suc  12261  nn0n0n1ge2b  12579  xnn0xr  12588  xnn0nemnf  12594  nn0lt10b  12664  nn0ind-raph  12702  elnn1uz2  12955  indstr2  12957  uzsupss  12970  rpnnen1lem4  13010  rpnnen1lem5  13011  xrnemnf  13148  xrnepnf  13149  mnfltxr  13158  xnn0n0n1ge2b  13163  xnn0ge0  13165  xrlttri  13170  xrlttr  13171  xrleid  13182  qbtwnxr  13232  xmullem2  13297  xlemul1a  13320  xrub  13344  reltxrnmnf  13375  ixxun  13394  xnn0xrge0  13539  fztpval  13621  fseq1p1m1  13633  elfznelfzob  13810  ltweuz  14004  fzfi  14015  fsuppmapnn0fiubex  14035  ser0f  14098  0exp  14140  faclbnd4lem1  14336  bcn1  14356  hashnemnf  14387  hashv01gt1  14388  hashsnle1  14461  hashgt12el2  14467  hashpw  14480  hashf1  14501  fz1isolem  14505  hash2prb  14516  hash3tpb  14539  0wrd0  14584  wrdlen1  14598  ccatvalfn  14625  eqs1  14657  wrdl1exs1  14658  swrdlen  14692  swrdwrdsymb  14707  swrdspsleq  14710  cats1un  14765  wrdind  14766  wrd2ind  14767  swrdccatin1  14769  repswsymballbi  14824  cshw1  14866  scshwfzeqfzo  14870  wrdl2exs2  14990  trclfvcotr  15053  relexp1g  15070  relexp0rel  15081  relexprelg  15082  relexpreld  15084  sgnmulsgn  15153  sqrt0  15299  sqrtsq  15327  mptfzshft  15836  prodf1f  15953  egt2lt3  16268  0dvds  16340  nn0onn  16444  nn0o  16447  divalgmod  16470  flodddiv4  16479  bitsp1o  16497  gcddvds  16567  bezout  16607  lcmdvds  16672  rpdvds  16724  1nprm  16743  prmind2  16749  dvdszzq  16786  nnoddn2prmb  16879  pcpre1  16908  vdwapf  17038  vdwapid1  17041  ram0  17088  ramz  17091  prmolefac  17112  cshws0  17167  prmlem0  17171  strle1  17224  restsspw  17490  prdsdsfn  17524  imasdsfn  17574  imasaddfnlem  17588  imasvscafn  17597  xpsfrnel  17622  isacs1i  17719  cidfn  17741  fnhomeqhomf  17753  comffn  17767  isoval  17828  sscres  17886  cofucl  17951  idffth  17998  ressffth  18003  cat1lem  18159  catcoppccl  18180  estrchomfn  18197  funcestrcsetclem4  18205  funcestrcsetclem7  18208  equivestrcsetc  18214  funcsetcestrclem4  18220  funcsetcestrclem7  18223  1stfcl  18259  2ndfcl  18260  prfcl  18265  evlfcl  18284  curf1cl  18290  curfcl  18294  hofcl  18321  yonedainv  18343  pospo  18405  lubfun  18412  glbfun  18425  joindmss  18439  meetdmss  18453  ipopos  18598  acsficl2d  18614  dirref  18663  mgmidcl  18730  mgmlrid  18731  ielefmnd  18952  smndex1basss  18973  smndex1n0mnd  18980  cntzssv  19404  idresperm  19462  symgvalstruct  19473  pmtrfmvdn0  19538  symggen  19546  psgnunilem1  19569  psgnprfval  19597  slwpgp  19689  frgpmhm  19841  frgpuptinv  19847  frgpup3lem  19853  gsumzoppg  20020  gsumcom2  20051  c0snmhm  20552  srhmsubc  20790  rhmsubclem1  20795  rrgsupp  20811  abv0  20937  zrhrhm  21672  psgnodpmr  21751  frlmphllem  21941  ellspd  21963  psrvscafval  22109  psrridm  22123  ltbwe  22206  psrbag0  22224  psrbagsn  22225  subrgascl  22228  psdmul  22340  mattpostpos  22622  mavmul0  22720  mavmul0g  22721  mdet0f1o  22761  m1detdiag  22765  m2detleiblem5  22793  m2detleiblem6  22794  m2detleiblem3  22797  m2detleiblem4  22798  maducoeval2  22808  d1mat2pmat  22907  chpmat1dlem  23003  chpmat1d  23004  baspartn  23122  eltg3  23130  topnex  23164  fctop  23172  cctop  23174  discld  23257  mretopd  23260  neipeltop  23297  neitr  23348  restcls  23349  ordtbaslem  23356  ordtuni  23358  idcn  23425  cnrmi  23528  cmpsublem  23567  cmpsub  23568  tgcmp  23569  uncmp  23571  hauscmplem  23574  cmpfi  23576  bwth  23578  1stcrestlem  23620  disllycmp  23666  dis1stc  23667  refref  23681  kgeni  23705  1stckgenlem  23721  kqffn  23893  snfil  24032  filconn  24051  cfinfil  24061  ufileu  24087  filufint  24088  fixufil  24090  cfinufil  24096  ufilen  24098  fin1aufil  24100  fmf  24113  rnelfm  24121  flimclslem  24152  hauspwpwf1  24155  supnfcls  24188  flimfnfcls  24196  fclscmp  24198  alexsubALTlem2  24216  alexsubALTlem3  24217  alexsubALT  24219  ptcmplem1  24220  cnextrel  24231  tsmsfbas  24296  ustref  24387  trust  24397  restutop  24405  isusp  24429  xmet0  24510  imasdsf1olem  24541  blfvalps  24551  blfps  24574  blf  24575  restmetu  24738  dscmet  24740  isngp2  24765  nm0  24797  nrginvrcn  24860  nmoix  24897  qdensere  24937  iccconn  24999  iccpnfcnv  25114  xrhmeo  25116  lebnumlem3  25133  metsscmetcld  25485  bcthlem5  25498  csschl  25546  rrxmfval  25576  minveclem3b  25598  cniccbdd  25631  ovolicc2lem4  25690  iunmbl  25723  ioorinv  25746  ioorcl  25747  i1f1lem  25859  limcvallem  26041  ellimc2  26047  limccnp  26061  limccnp2  26062  limcco  26063  perfdvf  26073  recnprss  26074  fncpn  26103  dvcmulf  26115  c1lip1  26167  lhop2  26185  q1pcl  26325  r1pdeglt  26328  ply1remlem  26333  plyssc  26368  ulm0  26565  cxpeq0  26854  cxplea  26872  cxplogb  26962  asinlem  27044  isppw2  27290  muval2  27309  dchrfi  27430  dchrpt  27442  bposlem6  27464  lgsdir2lem2  27501  lgsqr  27526  gausslemma2dlem4  27544  2lgslem2  27570  2lgslem3  27579  2lgs  27582  2sqlem7  27599  2sqlem11  27604  chtppilim  27650  nosgnn0i  27834  nolesgn2ores  27847  nogesgn1ores  27849  nosepnelem  27854  nosepdmlem  27858  nosupbnd1lem3  27885  nosupbnd1lem5  27887  nosupbnd2lem1  27890  noinfbnd1lem3  27900  noinfbnd1lem5  27902  noinfbnd2lem1  27905  oldval  28038  made0  28067  lrrecpo  28145  pncan2s  28278  divscan3d  28440  abssor  28450  om2noseqfo  28502  noseqrdglem  28509  noseqrdgfn  28510  noseqrdg0  28511  onsfi  28560  nohalf  28628  expsne0  28640  pw2divscan3d  28645  tgldimor  28782  tgcgr4  28811  tglnfn  28827  tglnunirn  28828  mirne  28955  mircinv  28956  perpln1  29001  perpln2  29002  tgplnfn  29068  lmiisolem  29116  prlngmid2  29222  xmstrkgc  29246  axcgrtr  29276  axsegconlem9  29286  axlowdimlem5  29307  axlowdimlem17  29319  axlowdim1  29320  uhgr0e  29432  edglnl  29504  uhgr0edgfi  29601  issubgr2  29633  subgrprop2  29635  egrsubgr  29638  0grsubgr  29639  0uhgrsubgr  29640  uhgrsubgrself  29641  nbgr1vtx  29719  nbgrssovtx  29722  nb3grprlem1  29741  uvtx01vtx  29758  cplgr1vlem  29790  cplgr1v  29791  usgrexilem  29801  wlkcomp  29991  wlk1walk  29999  wlkp1lem5  30036  uhgrwkspthlem1  30113  pthdlem1  30126  clwlkcomp  30139  lfgrn1cycl  30165  uspgrn2crct  30168  wwlksn0s  30221  usgrwwlks2on  30318  umgrwwlks2on  30319  clwwlkn  30388  clwwlkn1  30403  0ewlk  30476  1ewlk  30477  0spth  30488  upgr1wlkdlem2  30508  wlk2v2e  30519  upgr3v3e3cycl  30542  upgr4cycl4dv4e  30547  eupth0  30576  frgr0v  30624  frgr1v  30633  1vwmgr  30638  ex-opab  30794  grpoinvf  30895  nvmid  31022  nmlnoubi  31159  hiidrcl  31458  hsn0elch  31611  shjshseli  31856  cmbr4i  31964  dfiop2  32116  kbpj  32319  nmopun  32377  adjeq0  32454  kbass2  32480  pjssdif1i  32538  pjinvari  32554  pjcmul2i  32565  pj3i  32571  stge1i  32601  stle0i  32602  sumdmdlem2  32782  dmdbr6ati  32786  dmdbr7ati  32787  rabsnel  32857  unidifsnel  32892  unidifsnne  32893  disjdifprg  32931  ofoprabco  33020  padct  33074  fpwrelmapffslem  33088  nn0mnfxrd  33107  xrlelttric  33108  xnn0gt0  33125  iundisj2cnt  33155  f1ocnt  33156  fz1nnct  33157  fz1nntr  33158  hashxpe  33163  nn0min  33176  sgnmulsgp  33187  wrdt2ind  33282  xrge0tsmsbi  33403  opprabs  33773  rtelextdg2lem  34125  2sqr3minply  34179  locfinref  34240  dispcmp  34258  zartopn  34274  zarcmplem  34280  pstmxmet  34296  xrge0iifcnv  34332  xrge0iif1  34337  qqhre  34419  esumcl  34429  esumpr2  34466  esumpinfval  34472  esumpcvgval  34477  ofcfn  34499  pwsiga  34529  prsiga  34530  sigainb  34535  ldgenpisyslem1  34562  measiuns  34616  relfae  34646  pmeasmono  34723  sitgf  34746  eulerpartgbij  34771  signswch  34957  signslema  34958  signstlen  34963  signstfvn  34965  circlevma  35038  bnj216  35130  bnj151  35274  bnj517  35282  bnj970  35344  bnj1145  35390  bnj1498  35458  r1omhfb  35517  rankscottu  35531  fineqvrep  35535  fineqvac  35537  fineqvnttrclselem1  35542  fineqvnttrclselem2  35543  fineqvnttrclse  35545  fineqvinfep  35546  r1omhfbregs  35558  kard0b  35580  rankkardu  35592  wevgblacfn  35603  vonf1osev  35604  0nn0m1nnn0  35612  pthhashvtx  35628  acycgr0v  35648  prclisacycgr  35651  umgracycusgr  35654  cusgracyclt3v  35656  subfacp1lem5  35684  erdszelem8  35698  kur14lem1  35706  indispconn  35734  cvmsss2  35774  satfvsuclem2  35860  satfrel  35867  satfrnmapom  35870  satfv0fun  35871  satf00  35874  satf0suclem  35875  fmlasuc0  35884  msubrn  36029  dfon2lem7  36287  brbigcup  36396  elsingles  36416  fnimage  36427  funpartlem  36442  dfrdg4  36451  imagesset  36453  altopthsn  36461  elaltxp  36475  ellines  36652  linethru  36653  rankeq1o  36671  elhf2  36675  hfninf  36686  nn0prpwlem  36861  fneref  36889  neibastop2lem  36899  limsucncmpi  36984  tz9.1tco  37022  bj-exlimmpbir  37577  curryset  37610  bj-snglex  37637  bj-axnul  37737  bj-restpw  37762  bj-inftyexpidisj  37882  topdifinffinlem  38021  relowlssretop  38037  rdgeqoa  38044  finxpreclem6  38070  fvineqsneq  38086  pibt2  38091  poimirlem23  38322  poimirlem29  38328  poimirlem31  38330  volsupnfl  38344  cnambfre  38347  dvasin  38383  dvacos  38384  sdclem2  38421  sstotbnd2  38453  ssbnd  38467  ismgmOLD  38529  grpokerinj  38572  rngomndo  38614  isdrngo1  38635  ac6s6  38849  iss2  39021  relecxrn  39084  sucmapsuc  39166  cosselrels  39252  cnvelrels  39253  brssrid  39259  brcnvssrid  39264  dfdisjs5  39474  eldisjs5  39500  eldisjsim3  39614  mpets2  39632  pets  39643  prtlem12  39669  riotasv2d  39759  lkrscss  39900  islshpkrN  39922  isline  40541  ispointN  40544  0psubN  40551  linepsubN  40554  atpsubN  40555  cdlemk36  41715  diafn  41836  dibfna  41956  dibvalrel  41965  dicvalrelN  41987  diclspsn  41996  dihvalrel  42081  dih1  42088  lclkrlem1  42308  lclkr  42335  mapd1o  42450  mapdin  42464  hdmapfnN  42631  hgmapfnN  42690  lcmineqlem10  42833  sticksstones9  42949  sn-iotalem  43020  readvrec2  43150  readvrec  43151  repncan2  43171  elrfirn  43454  ismrcd1  43457  istopclsd  43459  rabren3dioph  43570  jm2.17b  43716  jm2.22  43750  jm2.23  43751  ttac  43791  pw2f1ocnv  43792  dnnumch1  43799  hbtlem5  43883  mncn0  43894  aaitgo  43917  rngunsnply  43924  unielss  43973  onexlimgt  43998  cantnfresb  44079  dflim5  44084  naddwordnexlem4  44156  safesnsupfiss  44169  safesnsupfidom1o  44171  safesnsupfilb  44172  ensucne0OLD  44284  clcnvlem  44377  relexp01min  44467  ntrf  44877  ssrecnpr  45046  seff  45047  sblpnf  45048  nzss  45055  dvconstbi  45072  ipo0  45186  ifr0  45187  addrfn  45208  subrfn  45209  mulvfn  45210  wfaxrep  45731  refsum2cnlem1  45785  rn1st  46016  ellimciota  46358  dvmptconst  46657  dvmptidg  46659  dvmulcncf  46667  dvdivcncf  46669  stoweidlem26  46768  stoweidlem50  46792  stoweidlem57  46799  aiotaval  47860  ndfatafv2nrn  47986  afv2ndefb  47989  funop1  48048  fun2dmnopgexmpl  48049  2ffzoeq  48093  2ltceilhalf  48097  m1modne  48119  iccpartiltu  48199  iccpartigtl  48200  zofldiv2ALTV  48455  evenprm2  48507  9fppr8  48530  stgoldbwt  48569  nnsum3primesle9  48587  nnsum4primeseven  48593  nnsum4primesevenALTV  48594  tgblthelfgott  48608  dfclnbgr6  48649  cycl3grtri  48740  grtrimap  48741  stgredgel  48750  stgr1  48754  isubgr3stgrlem2  48760  isubgr3stgrlem3  48761  usgrexmpl2trifr  48830  gpg5nbgrvtx13starlem1  48864  gpg5nbgrvtx13starlem2  48865  gpg5nbgrvtx13starlem3  48866  gpg5nbgr3star  48874  gpg3kgrtriex  48882  uspgrex  48943  0mgm  48959  nnsgrpmgm  48969  rngchomffvalALTV  49071  rhmsubcALTVlem1  49074  funcringcsetcALTV2lem4  49086  funcringcsetclem4ALTV  49109  srhmsubcALTV  49118  mapsnop  49152  zlmodzxzldeplem4  49311  zofldiv2  49339  fdivval  49347  nnlog2ge0lt1  49374  dig1  49416  itcoval2  49472  itcoval3  49473  mosn  49619  mo0  49620  mof02  49645  mofeu  49654  f102g  49658  f1mo  49659  tposres0  49683  f1omo  49699  f1omoOLD  49700  resipos  49781  intubeu  49790  unilbeu  49791  sectfn  49835  nelsubclem  49873  idfu1stf1o  49905  imaidfu  49916  oppfvallem  49941  funcoppc3  49953  idfth  49964  idsubc  49966  uptposlem  50003  swapf2fn  50074  swapf1f1o  50081  swapf2f1o  50082  swapf2f1oaALT  50084  fucof1  50128  fucofn2  50130  fucofn22  50146  reldmprcof1  50187  reldmprcof2  50188  fucoppcid  50214  fucoppc  50216  functhinclem1  50250  fullthinc  50256  thincciso  50259  indcthing  50266  indthinc  50268  indthincALT  50269  functermc  50314  discsntermlem  50376  reldmlan2  50423  reldmran2  50424  rellan  50429  relran  50430  termolmd  50476