Theorem mpbiri 258

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

Syntax hints:   → wi 4   ↔ wb 206

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 207

This theorem is referenced by:  elimh  1082  spei  2392  nfald2  2443  nfabd2  2915  raleleq  3315  raleleqOLD  3316  ceqsexv2d  3499  dedhb  3674  csbie2df  4406  ssdifeq0  4450  r19.2zb  4459  dedth  4547  pwidg  4583  snidg  4624  rexreusng  4643  exsnrex  4644  ifpr  4657  rmosn  4683  rabrsn  4688  prid1g  4724  tpid1g  4733  tpid2g  4735  tpid3g  4736  pwpw0  4777  sssn  4790  elpreqpr  4831  unimax  4908  intmin3  4940  eqbrtrdi  5146  al0ssb  5263  rabelpw  5291  intabs  5304  difelpw  5309  0inp0  5314  axpr  5382  intidg  5417  copsexgw  5450  copsexg  5451  euotd  5473  elopab  5487  elvvuni  5715  posn  5724  frsn  5726  eqrelriv  5752  relsnb  5765  relopabiALT  5786  opabid2  5791  ididg  5817  iss  6006  dfpo2  6269  ord0eln0  6388  sucidg  6415  nsuceq0  6417  funopg  6550  fn0  6649  f00  6742  f0bi  6743  f10d  6834  f1o00  6835  fo00  6836  brprcneu  6848  brprcneuALT  6849  dffn5  6919  fsn  7107  funop  7121  funsndifnop  7123  fnsnbOLD  7140  eufnfv  7203  f1ounsn  7247  f1eqcocnv  7276  nfriotadw  7352  nfriotad  7355  riotaprop  7371  oprabidw  7418  oprabid  7419  elrnmpo  7525  ov6g  7553  ovelrn  7565  caovmo  7626  offn  7666  caofinvl  7685  fr3nr  7748  onprc  7754  ordeleqon  7758  onint0  7767  0elsuc  7810  onuninsuci  7816  orduninsuc  7819  ordzsl  7821  onzsl  7822  tfinds  7836  limomss  7847  limom  7858  peano5  7869  xpexr  7894  eqop2  8011  opreuopreu  8013  1stconst  8079  2ndconst  8080  frxp2  8123  frxp3  8130  funsssuppss  8169  dftpos3  8223  dftpos4  8224  oawordeulem  8518  omwordi  8535  nnmwordi  8599  riiner  8763  ecopover  8794  map0g  8857  mapsnd  8859  elixpsn  8910  en0  8989  en0ALT  8990  en0r  8991  en1  8995  snfi  9014  fiprc  9016  sbthlem2  9052  sbthlem4  9054  sbthlem5  9055  0domg  9068  findcard  9127  findcard2  9128  nneneq  9170  sdom1  9189  sdom1OLD  9190  1sdom2dom  9194  fineqvlem  9209  nfielex  9218  enp1i  9224  elfiun  9381  marypha1lem  9384  oicl  9482  oif  9483  oion  9489  hartogslem1  9495  hartogs  9497  wemapso2  9506  card2on  9507  0wdom  9523  brwdom2  9526  inf3lem6  9586  cantnflem3  9644  cantnflem4  9645  wemapwe  9650  cnfcom  9653  ssttrcl  9668  ttrclselem2  9679  tctr  9693  r1tr  9729  r1rankidb  9757  r1pw  9798  scottex  9838  scott0  9839  bnd2  9846  eldju2ndl  9877  tskwe  9903  oncard  9913  cardlim  9925  harsdom  9948  en2eleq  9961  dfac8alem  9982  cardaleph  10042  iunfictbso  10067  infmap2  10170  ackbij1lem18  10189  cff  10201  cfsuc  10210  cff1  10211  cflim2  10216  cfss  10218  sdom2en01  10255  infpssrlem4  10259  fin23lem7  10269  fin23lem11  10270  isfin2-2  10272  fin23lem26  10278  fin23lem19  10289  fin23lem17  10291  isf34lem2  10326  isf34lem4  10330  fin1a2lem6  10358  fin1a2lem10  10362  fin1a2lem12  10364  itunifn  10370  hsmexlem1  10379  axcc2lem  10389  dcomex  10400  axdc3lem4  10406  ondomon  10516  konigthlem  10521  pwcfsdom  10536  cfpwsdom  10537  axpowndlem3  10552  canth4  10600  canthnumlem  10601  canthwelem  10603  canthwe  10604  canthp1lem2  10606  pwfseqlem4  10615  pwfseqlem5  10616  gchaleph  10624  gch2  10628  winainflem  10646  0tsk  10708  rankcf  10730  tskcard  10734  gruina  10771  grutsk  10775  tskmid  10793  indpi  10860  nqereu  10882  mulcanenq  10913  recmulnq  10917  archnq  10933  ltsopr  10985  1ne0sr  11049  0idsr  11050  00sr  11052  leid  11270  lelttric  11281  divcan3  11863  divid  11868  div0  11870  lemul1a  12036  nn1suc  12208  nn0n0n1ge2b  12511  xnn0xr  12520  xnn0nemnf  12526  nn0lt10b  12596  nn0ind-raph  12634  elnn1uz2  12884  indstr2  12886  uzsupss  12899  rpnnen1lem4  12939  rpnnen1lem5  12940  xrnemnf  13077  xrnepnf  13078  mnfltxr  13087  xnn0n0n1ge2b  13092  xnn0ge0  13094  xrlttri  13099  xrlttr  13100  xrleid  13111  qbtwnxr  13160  xmullem2  13225  xlemul1a  13248  xrub  13272  reltxrnmnf  13303  ixxun  13322  xnn0xrge0  13467  fztpval  13547  fseq1p1m1  13559  elfznelfzob  13734  ltweuz  13926  fzfi  13937  fsuppmapnn0fiubex  13957  ser0f  14020  0exp  14062  faclbnd4lem1  14258  bcn1  14278  hashnemnf  14309  hashv01gt1  14310  hashsnle1  14382  hashgt12el2  14388  hashpw  14401  hashf1  14422  fz1isolem  14426  hash2prb  14437  hash3tpb  14460  0wrd0  14505  wrdlen1  14519  ccatvalfn  14546  eqs1  14577  wrdl1exs1  14578  swrdlen  14612  swrdwrdsymb  14627  swrdspsleq  14630  cats1un  14686  wrdind  14687  wrd2ind  14688  swrdccatin1  14690  repswsymballbi  14745  cshw1  14787  scshwfzeqfzo  14792  wrdl2exs2  14912  trclfvcotr  14975  relexp1g  14992  relexp0rel  15003  relexprelg  15004  relexpreld  15006  sqrt0  15207  sqrtsq  15235  mptfzshft  15744  prodf1f  15858  egt2lt3  16174  0dvds  16246  nn0onn  16350  nn0o  16353  divalgmod  16376  flodddiv4  16385  bitsp1o  16403  gcddvds  16473  bezout  16513  lcmdvds  16578  rpdvds  16630  1nprm  16649  prmind2  16655  dvdszzq  16691  nnoddn2prmb  16784  pcpre1  16813  vdwapf  16943  vdwapid1  16946  ram0  16993  ramz  16996  prmolefac  17017  cshws0  17072  prmlem0  17076  strle1  17128  restsspw  17394  prdsdsfn  17428  imasdsfn  17477  imasaddfnlem  17491  imasvscafn  17500  xpsfrnel  17525  isacs1i  17618  cidfn  17640  fnhomeqhomf  17652  comffn  17666  isoval  17727  sscres  17785  cofucl  17850  idffth  17897  ressffth  17902  cat1lem  18058  catcoppccl  18079  estrchomfn  18096  funcestrcsetclem4  18104  funcestrcsetclem7  18107  equivestrcsetc  18113  funcsetcestrclem4  18119  funcsetcestrclem7  18122  1stfcl  18158  2ndfcl  18159  prfcl  18164  evlfcl  18183  curf1cl  18189  curfcl  18193  hofcl  18220  yonedainv  18242  pospo  18304  lubfun  18311  glbfun  18324  joindmss  18338  meetdmss  18352  ipopos  18495  acsficl2d  18511  dirref  18560  mgmidcl  18593  mgmlrid  18594  ielefmnd  18814  smndex1basss  18832  smndex1n0mnd  18839  cntzssv  19260  idresperm  19316  symgvalstruct  19327  pmtrfmvdn0  19392  symggen  19400  psgnunilem1  19423  psgnprfval  19451  slwpgp  19543  frgpmhm  19695  frgpuptinv  19701  frgpup3lem  19707  gsumzoppg  19874  gsumcom2  19905  c0snmhm  20372  srhmsubc  20589  rhmsubclem1  20594  rrgsupp  20610  abv0  20732  zrhrhm  21421  psgnodpmr  21499  frlmphllem  21689  ellspd  21711  psrvscafval  21857  psrridm  21872  ltbwe  21951  psrbag0  21969  psrbagsn  21970  subrgascl  21973  psdmul  22053  mattpostpos  22341  mavmul0  22439  mavmul0g  22440  mdet0f1o  22480  m1detdiag  22484  m2detleiblem5  22512  m2detleiblem6  22513  m2detleiblem3  22516  m2detleiblem4  22517  maducoeval2  22527  d1mat2pmat  22626  chpmat1dlem  22722  chpmat1d  22723  baspartn  22841  eltg3  22849  topnex  22883  fctop  22891  cctop  22893  discld  22976  mretopd  22979  neipeltop  23016  neitr  23067  restcls  23068  ordtbaslem  23075  ordtuni  23077  idcn  23144  cnrmi  23247  cmpsublem  23286  cmpsub  23287  tgcmp  23288  uncmp  23290  hauscmplem  23293  cmpfi  23295  bwth  23297  1stcrestlem  23339  disllycmp  23385  dis1stc  23386  refref  23400  kgeni  23424  1stckgenlem  23440  kqffn  23612  snfil  23751  filconn  23770  cfinfil  23780  ufileu  23806  filufint  23807  fixufil  23809  cfinufil  23815  ufilen  23817  fin1aufil  23819  fmf  23832  rnelfm  23840  flimclslem  23871  hauspwpwf1  23874  supnfcls  23907  flimfnfcls  23915  fclscmp  23917  alexsubALTlem2  23935  alexsubALTlem3  23936  alexsubALT  23938  ptcmplem1  23939  cnextrel  23950  tsmsfbas  24015  ustref  24106  trust  24117  restutop  24125  isusp  24149  xmet0  24230  imasdsf1olem  24261  blfvalps  24271  blfps  24294  blf  24295  restmetu  24458  dscmet  24460  isngp2  24485  nm0  24517  nrginvrcn  24580  nmoix  24617  qdensere  24657  iccconn  24719  iccpnfcnv  24842  xrhmeo  24844  lebnumlem3  24862  metsscmetcld  25215  bcthlem5  25228  csschl  25276  rrxmfval  25306  minveclem3b  25328  cniccbdd  25362  ovolicc2lem4  25421  iunmbl  25454  ioorinv  25477  ioorcl  25478  i1f1lem  25590  limcvallem  25772  ellimc2  25778  limccnp  25792  limccnp2  25793  limcco  25794  perfdvf  25804  recnprss  25805  fncpn  25835  dvcmulf  25848  c1lip1  25902  lhop2  25920  q1pcl  26062  r1pdeglt  26065  ply1remlem  26070  plyssc  26105  ulm0  26300  cxpeq0  26587  cxplea  26605  cxplogb  26696  asinlem  26778  isppw2  27025  muval2  27044  dchrfi  27166  dchrpt  27178  bposlem6  27200  lgsdir2lem2  27237  lgsqr  27262  gausslemma2dlem4  27280  2lgslem2  27306  2lgslem3  27315  2lgs  27318  2sqlem7  27335  2sqlem11  27340  chtppilim  27386  nosgnn0i  27571  nolesgn2ores  27584  nogesgn1ores  27586  nosepnelem  27591  nosepdmlem  27595  nosupbnd1lem3  27622  nosupbnd1lem5  27624  nosupbnd2lem1  27627  noinfbnd1lem3  27637  noinfbnd1lem5  27639  noinfbnd2lem1  27642  oldval  27762  made0  27785  lrrecpo  27848  pncan2s  27978  divscan3d  28138  abssor  28148  om2noseqfo  28192  noseqrdglem  28199  noseqrdgfn  28200  noseqrdg0  28201  onsfi  28247  nohalf  28310  expsne0  28321  pw2divscan3d  28326  tgldimor  28429  tgcgr4  28458  tglnfn  28474  tglnunirn  28475  mirne  28594  mircinv  28595  perpln1  28637  perpln2  28638  lmiisolem  28723  xmstrkgc  28813  axcgrtr  28842  axsegconlem9  28852  axlowdimlem5  28873  axlowdimlem17  28885  axlowdim1  28886  uhgr0e  28998  edglnl  29070  uhgr0edgfi  29167  issubgr2  29199  subgrprop2  29201  egrsubgr  29204  0grsubgr  29205  0uhgrsubgr  29206  uhgrsubgrself  29207  nbgr1vtx  29285  nbgrssovtx  29288  nb3grprlem1  29307  uvtx01vtx  29324  cplgr1vlem  29356  cplgr1v  29357  usgrexilem  29367  wlkcomp  29559  wlk1walk  29567  wlkp1lem5  29605  uhgrwkspthlem1  29683  pthdlem1  29696  clwlkcomp  29709  lfgrn1cycl  29735  uspgrn2crct  29738  wwlksn0s  29791  umgrwwlks2on  29887  clwwlkn  29955  clwwlkn1  29970  0ewlk  30043  1ewlk  30044  0spth  30055  upgr1wlkdlem2  30075  wlk2v2e  30086  upgr3v3e3cycl  30109  upgr4cycl4dv4e  30114  eupth0  30143  frgr0v  30191  frgr1v  30200  1vwmgr  30205  ex-opab  30361  grpoinvf  30461  nvmid  30588  nmlnoubi  30725  hiidrcl  31024  hsn0elch  31177  shjshseli  31422  cmbr4i  31530  dfiop2  31682  kbpj  31885  nmopun  31943  adjeq0  32020  kbass2  32046  pjssdif1i  32104  pjinvari  32120  pjcmul2i  32131  pj3i  32137  stge1i  32167  stle0i  32168  sumdmdlem2  32348  dmdbr6ati  32352  dmdbr7ati  32353  rabsnel  32429  unidifsnel  32464  unidifsnne  32465  disjdifprg  32504  ofoprabco  32588  padct  32643  fpwrelmapffslem  32655  xrlelttric  32675  xnn0gt0  32692  iundisj2cnt  32722  f1ocnt  32725  fz1nnct  32726  fz1nntr  32727  hashxpe  32732  nn0min  32745  sgnmulsgn  32767  sgnmulsgp  32768  wrdt2ind  32875  xrge0tsmsbi  33003  opprabs  33453  rtelextdg2lem  33716  2sqr3minply  33770  locfinref  33831  dispcmp  33849  zartopn  33865  zarcmplem  33871  pstmxmet  33887  xrge0iifcnv  33923  xrge0iif1  33928  qqhre  34010  esumcl  34020  esumpr2  34057  esumpinfval  34063  esumpcvgval  34068  ofcfn  34090  pwsiga  34120  prsiga  34121  sigainb  34126  ldgenpisyslem1  34153  measiuns  34207  relfae  34237  pmeasmono  34315  sitgf  34338  eulerpartgbij  34363  signswch  34552  signslema  34553  signstlen  34558  signstfvn  34560  circlevma  34633  bnj216  34722  bnj151  34867  bnj517  34875  bnj970  34937  bnj1145  34983  bnj1498  35051  fineqvrep  35085  fineqvac  35087  wevgblacfn  35096  0nn0m1nnn0  35100  pthhashvtx  35115  acycgr0v  35135  prclisacycgr  35138  umgracycusgr  35141  cusgracyclt3v  35143  subfacp1lem5  35171  erdszelem8  35185  kur14lem1  35193  indispconn  35221  cvmsss2  35261  satfvsuclem2  35347  satfrel  35354  satfrnmapom  35357  satfv0fun  35358  satf00  35361  satf0suclem  35362  fmlasuc0  35371  msubrn  35516  dfon2lem7  35777  brbigcup  35886  elsingles  35906  fnimage  35917  funpartlem  35930  dfrdg4  35939  imagesset  35941  altopthsn  35949  elaltxp  35963  ellines  36140  linethru  36141  rankeq1o  36159  elhf2  36163  hfninf  36174  nn0prpwlem  36310  fneref  36338  neibastop2lem  36348  limsucncmpi  36433  bj-exlimmpbir  36902  curryset  36934  bj-snglex  36961  bj-restpw  37080  bj-inftyexpidisj  37198  topdifinffinlem  37335  relowlssretop  37351  rdgeqoa  37358  finxpreclem6  37384  fvineqsneq  37400  pibt2  37405  poimirlem23  37637  poimirlem29  37643  poimirlem31  37645  volsupnfl  37659  cnambfre  37662  dvasin  37698  dvacos  37699  sdclem2  37736  sstotbnd2  37768  ssbnd  37782  ismgmOLD  37844  grpokerinj  37887  rngomndo  37929  isdrngo1  37950  ac6s6  38166  iss2  38326  cnvelrels  38486  cosselrels  38487  brssrid  38493  brcnvssrid  38498  dfdisjs5  38704  eldisjs5  38718  mpets2  38833  pets  38844  prtlem12  38860  riotasv2d  38950  lkrscss  39091  islshpkrN  39113  isline  39733  ispointN  39736  0psubN  39743  linepsubN  39746  atpsubN  39747  cdlemk36  40907  diafn  41028  dibfna  41148  dibvalrel  41157  dicvalrelN  41179  diclspsn  41188  dihvalrel  41273  dih1  41280  lclkrlem1  41500  lclkr  41527  mapd1o  41642  mapdin  41656  hdmapfnN  41823  hgmapfnN  41882  lcmineqlem10  42026  sticksstones9  42142  sn-iotalem  42209  readvrec2  42349  readvrec  42350  repncan2  42370  elrfirn  42683  ismrcd1  42686  istopclsd  42688  rabren3dioph  42803  jm2.17b  42950  jm2.22  42984  jm2.23  42985  ttac  43025  pw2f1ocnv  43026  dnnumch1  43033  hbtlem5  43117  mncn0  43128  aaitgo  43151  rngunsnply  43158  unielss  43207  onexlimgt  43232  cantnfresb  43313  dflim5  43318  naddwordnexlem4  43390  safesnsupfiss  43404  safesnsupfidom1o  43406  safesnsupfilb  43407  ensucne0OLD  43519  clcnvlem  43612  relexp01min  43702  ntrf  44112  ssrecnpr  44297  seff  44298  sblpnf  44299  nzss  44306  dvconstbi  44323  ipo0  44438  ifr0  44439  addrfn  44461  subrfn  44462  mulvfn  44463  wfaxrep  44984  refsum2cnlem1  45031  rn1st  45267  ellimciota  45612  dvmptconst  45913  dvmptidg  45915  dvmulcncf  45923  dvdivcncf  45925  stoweidlem26  46024  stoweidlem50  46048  stoweidlem57  46055  aiotaval  47096  ndfatafv2nrn  47222  afv2ndefb  47225  funop1  47284  fun2dmnopgexmpl  47285  2ffzoeq  47328  2ltceilhalf  47329  m1modne  47349  iccpartiltu  47423  iccpartigtl  47424  zofldiv2ALTV  47663  evenprm2  47715  9fppr8  47738  stgoldbwt  47777  nnsum3primesle9  47795  nnsum4primeseven  47801  nnsum4primesevenALTV  47802  tgblthelfgott  47816  dfclnbgr6  47856  cycl3grtri  47946  grtrimap  47947  stgredgel  47956  stgr1  47960  isubgr3stgrlem2  47966  isubgr3stgrlem3  47967  usgrexmpl2trifr  48028  gpg5nbgrvtx13starlem1  48062  gpg5nbgrvtx13starlem2  48063  gpg5nbgrvtx13starlem3  48064  gpg5nbgr3star  48072  gpg3kgrtriex  48080  uspgrex  48138  0mgm  48154  nnsgrpmgm  48164  rngchomffvalALTV  48266  rhmsubcALTVlem1  48269  funcringcsetcALTV2lem4  48281  funcringcsetclem4ALTV  48304  srhmsubcALTV  48313  mapsnop  48332  zlmodzxzldeplem4  48492  zofldiv2  48520  fdivval  48528  nnlog2ge0lt1  48555  dig1  48597  itcoval2  48653  itcoval3  48654  mosn  48801  mo0  48802  mof02  48827  mofeu  48836  f102g  48840  f1mo  48841  tposres0  48865  f1omo  48881  f1omoOLD  48882  resipos  48963  intubeu  48972  unilbeu  48973  sectfn  49018  nelsubclem  49056  idfu1stf1o  49088  imaidfu  49099  oppfvallem  49124  funcoppc3  49136  idfth  49147  idsubc  49149  uptposlem  49186  swapf2fn  49257  swapf1f1o  49264  swapf2f1o  49265  swapf2f1oaALT  49267  fucof1  49311  fucofn2  49313  fucofn22  49329  reldmprcof1  49370  reldmprcof2  49371  fucoppcid  49397  fucoppc  49399  functhinclem1  49433  fullthinc  49439  thincciso  49442  indcthing  49449  indthinc  49451  indthincALT  49452  functermc  49497  discsntermlem  49559  reldmlan2  49606  reldmran2  49607  rellan  49612  relran  49613  termolmd  49659