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

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

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  1088  spei  2402  nfald2  2453  nfabd2  2925  raleleq  3310  raleleqOLD  3311  ceqsexv2d  3482  dedhb  3651  csbie2df  4378  ssdifeq0  4421  dedth  4520  pwidg  4556  snidg  4599  rexreusng  4618  exsnrex  4619  ifpr  4632  rmosn  4658  rabrsn  4663  prid1g  4699  tpid1g  4708  tpid2g  4710  tpid3g  4711  pwpw0  4751  sssn  4764  elpreqpr  4805  unimax  4882  intmin3  4913  eqbrtrdi  5118  al0ssb  5237  vneqv  5245  rabelpw  5271  intabs  5284  difelpw  5289  0inp0  5294  axpr  5363  intidg  5403  copsexgw  5437  copsexgwOLD  5438  copsexg  5439  euotd  5461  elopab  5476  elvvuni  5702  posn  5711  frsn  5713  eqrelriv  5739  relsnb  5752  relopabiALT  5773  opabid2  5778  ididg  5802  iss  5994  dfpo2  6254  ord0eln0  6373  sucidg  6400  nsuceq0  6402  funopg  6526  fn0  6623  f00  6716  f0bi  6717  f10d  6808  f1o00  6809  fo00  6810  brprcneu  6824  brprcneuALT  6825  dffn5  6892  fsn  7084  funop  7099  funsndifnop  7101  fnsnbOLD  7117  eufnfv  7180  f1ounsn  7223  f1eqcocnv  7252  nfriotadw  7328  nfriotad  7331  riotaprop  7347  oprabidw  7394  oprabid  7395  elrnmpo  7499  ov6g  7527  ovelrn  7539  caovmo  7600  offn  7640  caofinvl  7659  fr3nr  7722  onprc  7728  ordeleqon  7732  onint0  7741  0elsuc  7782  onuninsuci  7787  orduninsuc  7790  ordzsl  7792  onzsl  7793  tfinds  7807  limomss  7818  limom  7829  peano5  7840  xpexr  7865  eqop2  7981  opreuopreu  7983  1stconst  8046  2ndconst  8047  frxp2  8091  frxp3  8098  funsssuppss  8137  dftpos3  8191  dftpos4  8192  oawordeulem  8486  omwordi  8503  nnmwordi  8568  riiner  8734  ecopover  8765  map0g  8829  mapsnd  8831  elixpsn  8882  en0  8962  en0ALT  8963  en0r  8964  en1  8968  snfi  8987  fiprc  8988  sbthlem2  9023  sbthlem4  9025  sbthlem5  9026  0domg  9039  findcard  9095  findcard2  9096  nneneq  9137  sdom1  9157  1sdom2dom  9161  fineqvlem  9173  nfielex  9181  enp1i  9186  elfiun  9340  marypha1lem  9343  oicl  9441  oif  9442  oion  9448  hartogslem1  9454  hartogs  9456  wemapso2  9465  card2on  9466  0wdom  9482  brwdom2  9485  elirrv  9509  inf3lem6  9552  cantnflem3  9610  cantnflem4  9611  wemapwe  9616  cnfcom  9619  ssttrcl  9634  ttrclselem2  9645  tctr  9657  r1tr  9698  r1rankidb  9726  r1pw  9767  scottex  9807  scott0  9808  bnd2  9815  eldju2ndl  9846  tskwe  9872  oncard  9882  cardlim  9894  harsdom  9917  en2eleq  9928  dfac8alem  9949  cardaleph  10009  iunfictbso  10034  infmap2  10137  ackbij1lem18  10156  cff  10168  cfsuc  10177  cff1  10178  cflim2  10183  cfss  10185  sdom2en01  10222  infpssrlem4  10226  fin23lem7  10236  fin23lem11  10237  isfin2-2  10239  fin23lem26  10245  fin23lem19  10256  fin23lem17  10258  isf34lem2  10293  isf34lem4  10297  fin1a2lem6  10325  fin1a2lem10  10329  fin1a2lem12  10331  itunifn  10337  hsmexlem1  10346  axcc2lem  10356  dcomex  10367  axdc3lem4  10373  ondomon  10483  konigthlem  10489  pwcfsdom  10504  cfpwsdom  10505  axpowndlem3  10520  canth4  10568  canthnumlem  10569  canthwelem  10571  canthwe  10572  canthp1lem2  10574  pwfseqlem4  10583  pwfseqlem5  10584  gchaleph  10592  gch2  10596  winainflem  10614  0tsk  10676  rankcf  10698  tskcard  10702  gruina  10739  grutsk  10743  tskmid  10761  indpi  10828  nqereu  10850  mulcanenq  10881  recmulnq  10885  archnq  10901  ltsopr  10953  1ne0sr  11017  0idsr  11018  00sr  11020  leid  11240  lelttric  11251  divcan3  11833  divid  11838  div0  11840  lemul1a  12007  nn1suc  12194  nn0n0n1ge2b  12504  xnn0xr  12513  xnn0nemnf  12519  nn0lt10b  12589  nn0ind-raph  12627  elnn1uz2  12873  indstr2  12875  uzsupss  12888  rpnnen1lem4  12928  rpnnen1lem5  12929  xrnemnf  13066  xrnepnf  13067  mnfltxr  13076  xnn0n0n1ge2b  13081  xnn0ge0  13083  xrlttri  13088  xrlttr  13089  xrleid  13100  qbtwnxr  13150  xmullem2  13215  xlemul1a  13238  xrub  13262  reltxrnmnf  13293  ixxun  13312  xnn0xrge0  13457  fztpval  13538  fseq1p1m1  13550  elfznelfzob  13727  ltweuz  13921  fzfi  13932  fsuppmapnn0fiubex  13952  ser0f  14015  0exp  14057  faclbnd4lem1  14253  bcn1  14273  hashnemnf  14304  hashv01gt1  14305  hashsnle1  14377  hashgt12el2  14383  hashpw  14396  hashf1  14417  fz1isolem  14421  hash2prb  14432  hash3tpb  14455  0wrd0  14500  wrdlen1  14514  ccatvalfn  14541  eqs1  14573  wrdl1exs1  14574  swrdlen  14608  swrdwrdsymb  14623  swrdspsleq  14626  cats1un  14681  wrdind  14682  wrd2ind  14683  swrdccatin1  14685  repswsymballbi  14740  cshw1  14782  scshwfzeqfzo  14786  wrdl2exs2  14906  trclfvcotr  14969  relexp1g  14986  relexp0rel  14997  relexprelg  14998  relexpreld  15000  sqrt0  15201  sqrtsq  15229  mptfzshft  15738  prodf1f  15855  egt2lt3  16171  0dvds  16243  nn0onn  16347  nn0o  16350  divalgmod  16373  flodddiv4  16382  bitsp1o  16400  gcddvds  16470  bezout  16510  lcmdvds  16575  rpdvds  16627  1nprm  16646  prmind2  16652  dvdszzq  16689  nnoddn2prmb  16782  pcpre1  16811  vdwapf  16941  vdwapid1  16944  ram0  16991  ramz  16994  prmolefac  17015  cshws0  17070  prmlem0  17074  strle1  17126  restsspw  17392  prdsdsfn  17426  imasdsfn  17476  imasaddfnlem  17490  imasvscafn  17499  xpsfrnel  17524  isacs1i  17621  cidfn  17643  fnhomeqhomf  17655  comffn  17669  isoval  17730  sscres  17788  cofucl  17853  idffth  17900  ressffth  17905  cat1lem  18061  catcoppccl  18082  estrchomfn  18099  funcestrcsetclem4  18107  funcestrcsetclem7  18110  equivestrcsetc  18116  funcsetcestrclem4  18122  funcsetcestrclem7  18125  1stfcl  18161  2ndfcl  18162  prfcl  18167  evlfcl  18186  curf1cl  18192  curfcl  18196  hofcl  18223  yonedainv  18245  pospo  18307  lubfun  18314  glbfun  18327  joindmss  18341  meetdmss  18355  ipopos  18500  acsficl2d  18516  dirref  18565  mgmidcl  18632  mgmlrid  18633  ielefmnd  18853  smndex1basss  18874  smndex1n0mnd  18881  cntzssv  19301  idresperm  19359  symgvalstruct  19370  pmtrfmvdn0  19435  symggen  19443  psgnunilem1  19466  psgnprfval  19494  slwpgp  19586  frgpmhm  19738  frgpuptinv  19744  frgpup3lem  19750  gsumzoppg  19917  gsumcom2  19948  c0snmhm  20441  srhmsubc  20659  rhmsubclem1  20664  rrgsupp  20680  abv0  20802  zrhrhm  21493  psgnodpmr  21572  frlmphllem  21762  ellspd  21784  psrvscafval  21930  psrridm  21944  ltbwe  22027  psrbag0  22045  psrbagsn  22046  subrgascl  22049  psdmul  22161  mattpostpos  22444  mavmul0  22542  mavmul0g  22543  mdet0f1o  22583  m1detdiag  22587  m2detleiblem5  22615  m2detleiblem6  22616  m2detleiblem3  22619  m2detleiblem4  22620  maducoeval2  22630  d1mat2pmat  22729  chpmat1dlem  22825  chpmat1d  22826  baspartn  22944  eltg3  22952  topnex  22986  fctop  22994  cctop  22996  discld  23079  mretopd  23082  neipeltop  23119  neitr  23170  restcls  23171  ordtbaslem  23178  ordtuni  23180  idcn  23247  cnrmi  23350  cmpsublem  23389  cmpsub  23390  tgcmp  23391  uncmp  23393  hauscmplem  23396  cmpfi  23398  bwth  23400  1stcrestlem  23442  disllycmp  23488  dis1stc  23489  refref  23503  kgeni  23527  1stckgenlem  23543  kqffn  23715  snfil  23854  filconn  23873  cfinfil  23883  ufileu  23909  filufint  23910  fixufil  23912  cfinufil  23918  ufilen  23920  fin1aufil  23922  fmf  23935  rnelfm  23943  flimclslem  23974  hauspwpwf1  23977  supnfcls  24010  flimfnfcls  24018  fclscmp  24020  alexsubALTlem2  24038  alexsubALTlem3  24039  alexsubALT  24041  ptcmplem1  24042  cnextrel  24053  tsmsfbas  24118  ustref  24209  trust  24219  restutop  24227  isusp  24251  xmet0  24332  imasdsf1olem  24363  blfvalps  24373  blfps  24396  blf  24397  restmetu  24560  dscmet  24562  isngp2  24587  nm0  24619  nrginvrcn  24682  nmoix  24719  qdensere  24759  iccconn  24821  iccpnfcnv  24936  xrhmeo  24938  lebnumlem3  24955  metsscmetcld  25307  bcthlem5  25320  csschl  25368  rrxmfval  25398  minveclem3b  25420  cniccbdd  25453  ovolicc2lem4  25512  iunmbl  25545  ioorinv  25568  ioorcl  25569  i1f1lem  25681  limcvallem  25863  ellimc2  25869  limccnp  25883  limccnp2  25884  limcco  25885  perfdvf  25895  recnprss  25896  fncpn  25925  dvcmulf  25937  c1lip1  25989  lhop2  26007  q1pcl  26147  r1pdeglt  26150  ply1remlem  26155  plyssc  26190  ulm0  26381  cxpeq0  26667  cxplea  26685  cxplogb  26775  asinlem  26857  isppw2  27103  muval2  27122  dchrfi  27243  dchrpt  27255  bposlem6  27277  lgsdir2lem2  27314  lgsqr  27339  gausslemma2dlem4  27357  2lgslem2  27383  2lgslem3  27392  2lgs  27395  2sqlem7  27412  2sqlem11  27417  chtppilim  27463  nosgnn0i  27648  nolesgn2ores  27661  nogesgn1ores  27663  nosepnelem  27668  nosepdmlem  27672  nosupbnd1lem3  27699  nosupbnd1lem5  27701  nosupbnd2lem1  27704  noinfbnd1lem3  27714  noinfbnd1lem5  27716  noinfbnd2lem1  27719  oldval  27851  made0  27880  lrrecpo  27958  pncan2s  28091  divscan3d  28253  abssor  28263  om2noseqfo  28315  noseqrdglem  28322  noseqrdgfn  28323  noseqrdg0  28324  onsfi  28373  nohalf  28441  expsne0  28453  pw2divscan3d  28458  tgldimor  28595  tgcgr4  28624  tglnfn  28640  tglnunirn  28641  mirne  28760  mircinv  28761  perpln1  28803  perpln2  28804  lmiisolem  28889  xmstrkgc  28979  axcgrtr  29009  axsegconlem9  29019  axlowdimlem5  29040  axlowdimlem17  29052  axlowdim1  29053  uhgr0e  29165  edglnl  29237  uhgr0edgfi  29334  issubgr2  29366  subgrprop2  29368  egrsubgr  29371  0grsubgr  29372  0uhgrsubgr  29373  uhgrsubgrself  29374  nbgr1vtx  29452  nbgrssovtx  29455  nb3grprlem1  29474  uvtx01vtx  29491  cplgr1vlem  29523  cplgr1v  29524  usgrexilem  29534  wlkcomp  29724  wlk1walk  29732  wlkp1lem5  29769  uhgrwkspthlem1  29846  pthdlem1  29859  clwlkcomp  29872  lfgrn1cycl  29898  uspgrn2crct  29901  wwlksn0s  29954  usgrwwlks2on  30051  umgrwwlks2on  30052  clwwlkn  30121  clwwlkn1  30136  0ewlk  30209  1ewlk  30210  0spth  30221  upgr1wlkdlem2  30241  wlk2v2e  30252  upgr3v3e3cycl  30275  upgr4cycl4dv4e  30280  eupth0  30309  frgr0v  30357  frgr1v  30366  1vwmgr  30371  ex-opab  30527  grpoinvf  30628  nvmid  30755  nmlnoubi  30892  hiidrcl  31191  hsn0elch  31344  shjshseli  31589  cmbr4i  31697  dfiop2  31849  kbpj  32052  nmopun  32110  adjeq0  32187  kbass2  32213  pjssdif1i  32271  pjinvari  32287  pjcmul2i  32298  pj3i  32304  stge1i  32334  stle0i  32335  sumdmdlem2  32515  dmdbr6ati  32519  dmdbr7ati  32520  rabsnel  32595  unidifsnel  32630  unidifsnne  32631  disjdifprg  32671  ofoprabco  32763  padct  32817  fpwrelmapffslem  32831  nn0mnfxrd  32850  xrlelttric  32851  xnn0gt0  32868  iundisj2cnt  32898  f1ocnt  32899  fz1nnct  32900  fz1nntr  32901  hashxpe  32906  nn0min  32920  sgnmulsgn  32941  sgnmulsgp  32942  wrdt2ind  33039  xrge0tsmsbi  33162  opprabs  33572  rtelextdg2lem  33917  2sqr3minply  33971  locfinref  34032  dispcmp  34050  zartopn  34066  zarcmplem  34072  pstmxmet  34088  xrge0iifcnv  34124  xrge0iif1  34129  qqhre  34211  esumcl  34221  esumpr2  34258  esumpinfval  34264  esumpcvgval  34269  ofcfn  34291  pwsiga  34321  prsiga  34322  sigainb  34327  ldgenpisyslem1  34354  measiuns  34408  relfae  34438  pmeasmono  34515  sitgf  34538  eulerpartgbij  34563  signswch  34752  signslema  34753  signstlen  34758  signstfvn  34760  circlevma  34833  bnj216  34922  bnj151  35066  bnj517  35074  bnj970  35136  bnj1145  35182  bnj1498  35250  r1omhfb  35303  fineqvrep  35305  fineqvac  35307  fineqvnttrclselem1  35312  fineqvnttrclselem2  35313  fineqvnttrclse  35315  fineqvinfep  35316  r1omhfbregs  35328  wevgblacfn  35338  0nn0m1nnn0  35342  pthhashvtx  35357  acycgr0v  35377  prclisacycgr  35380  umgracycusgr  35383  cusgracyclt3v  35385  subfacp1lem5  35413  erdszelem8  35427  kur14lem1  35435  indispconn  35463  cvmsss2  35503  satfvsuclem2  35589  satfrel  35596  satfrnmapom  35599  satfv0fun  35600  satf00  35603  satf0suclem  35604  fmlasuc0  35613  msubrn  35758  dfon2lem7  36016  brbigcup  36125  elsingles  36145  fnimage  36156  funpartlem  36171  dfrdg4  36180  imagesset  36182  altopthsn  36190  elaltxp  36204  ellines  36381  linethru  36382  rankeq1o  36400  elhf2  36404  hfninf  36415  nn0prpwlem  36551  fneref  36579  neibastop2lem  36589  limsucncmpi  36674  tz9.1tco  36712  bj-exlimmpbir  37268  curryset  37300  bj-snglex  37327  bj-axnul  37426  bj-restpw  37451  bj-inftyexpidisj  37571  topdifinffinlem  37710  relowlssretop  37726  rdgeqoa  37733  finxpreclem6  37759  fvineqsneq  37775  pibt2  37780  poimirlem23  38011  poimirlem29  38017  poimirlem31  38019  volsupnfl  38033  cnambfre  38036  dvasin  38072  dvacos  38073  sdclem2  38110  sstotbnd2  38142  ssbnd  38156  ismgmOLD  38218  grpokerinj  38261  rngomndo  38303  isdrngo1  38324  ac6s6  38540  iss2  38712  relecxrn  38775  sucmapsuc  38857  cosselrels  38943  cnvelrels  38944  brssrid  38950  brcnvssrid  38955  dfdisjs5  39165  eldisjs5  39191  eldisjsim3  39305  mpets2  39323  pets  39334  prtlem12  39360  riotasv2d  39450  lkrscss  39591  islshpkrN  39613  isline  40232  ispointN  40235  0psubN  40242  linepsubN  40245  atpsubN  40246  cdlemk36  41406  diafn  41527  dibfna  41647  dibvalrel  41656  dicvalrelN  41678  diclspsn  41687  dihvalrel  41772  dih1  41779  lclkrlem1  41999  lclkr  42026  mapd1o  42141  mapdin  42155  hdmapfnN  42322  hgmapfnN  42381  lcmineqlem10  42524  sticksstones9  42640  sn-iotalem  42709  readvrec2  42839  readvrec  42840  repncan2  42860  elrfirn  43145  ismrcd1  43148  istopclsd  43150  rabren3dioph  43261  jm2.17b  43407  jm2.22  43441  jm2.23  43442  ttac  43482  pw2f1ocnv  43483  dnnumch1  43490  hbtlem5  43574  mncn0  43585  aaitgo  43608  rngunsnply  43615  unielss  43664  onexlimgt  43689  cantnfresb  43770  dflim5  43775  naddwordnexlem4  43847  safesnsupfiss  43860  safesnsupfidom1o  43862  safesnsupfilb  43863  ensucne0OLD  43975  clcnvlem  44068  relexp01min  44158  ntrf  44568  ssrecnpr  44753  seff  44754  sblpnf  44755  nzss  44762  dvconstbi  44779  ipo0  44893  ifr0  44894  addrfn  44916  subrfn  44917  mulvfn  44918  wfaxrep  45439  refsum2cnlem1  45486  rn1st  45718  ellimciota  46060  dvmptconst  46359  dvmptidg  46361  dvmulcncf  46369  dvdivcncf  46371  stoweidlem26  46470  stoweidlem50  46494  stoweidlem57  46501  aiotaval  47559  ndfatafv2nrn  47685  afv2ndefb  47688  funop1  47747  fun2dmnopgexmpl  47748  2ffzoeq  47792  2ltceilhalf  47796  m1modne  47818  iccpartiltu  47898  iccpartigtl  47899  zofldiv2ALTV  48154  evenprm2  48206  9fppr8  48229  stgoldbwt  48268  nnsum3primesle9  48286  nnsum4primeseven  48292  nnsum4primesevenALTV  48293  tgblthelfgott  48307  dfclnbgr6  48348  cycl3grtri  48439  grtrimap  48440  stgredgel  48449  stgr1  48453  isubgr3stgrlem2  48459  isubgr3stgrlem3  48460  usgrexmpl2trifr  48529  gpg5nbgrvtx13starlem1  48563  gpg5nbgrvtx13starlem2  48564  gpg5nbgrvtx13starlem3  48565  gpg5nbgr3star  48573  gpg3kgrtriex  48581  uspgrex  48642  0mgm  48658  nnsgrpmgm  48668  rngchomffvalALTV  48770  rhmsubcALTVlem1  48773  funcringcsetcALTV2lem4  48785  funcringcsetclem4ALTV  48808  srhmsubcALTV  48817  mapsnop  48836  zlmodzxzldeplem4  48995  zofldiv2  49023  fdivval  49031  nnlog2ge0lt1  49058  dig1  49100  itcoval2  49156  itcoval3  49157  mosn  49304  mo0  49305  mof02  49330  mofeu  49339  f102g  49343  f1mo  49344  tposres0  49368  f1omo  49384  f1omoOLD  49385  resipos  49466  intubeu  49475  unilbeu  49476  sectfn  49520  nelsubclem  49558  idfu1stf1o  49590  imaidfu  49601  oppfvallem  49626  funcoppc3  49638  idfth  49649  idsubc  49651  uptposlem  49688  swapf2fn  49759  swapf1f1o  49766  swapf2f1o  49767  swapf2f1oaALT  49769  fucof1  49813  fucofn2  49815  fucofn22  49831  reldmprcof1  49872  reldmprcof2  49873  fucoppcid  49899  fucoppc  49901  functhinclem1  49935  fullthinc  49941  thincciso  49944  indcthing  49951  indthinc  49953  indthincALT  49954  functermc  49999  discsntermlem  50061  reldmlan2  50108  reldmran2  50109  rellan  50114  relran  50115  termolmd  50161