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

Syntax hints:   → wi 4   ↔ wb 209

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 210

This theorem is referenced by:  elimh  1085  spei  2393  nfald2  2444  nfabd2  2923  raleleqALT  3324  dedhb  3606  sbceqal  3749  csbie2df  4341  ssdifeq0  4384  r19.2zb  4393  dedth  4483  pwidg  4521  elpr2OLD  4553  snidg  4561  rexreusng  4581  exsnrex  4582  ifpr  4593  rmosn  4621  rabrsn  4626  prid1g  4662  tpid1g  4671  tpid2g  4673  tpid3g  4674  pwpw0  4712  sssn  4725  elpreqpr  4763  pwsnOLD  4798  unimax  4843  intmin3  4873  eqbrtrdi  5078  al0ssb  5186  intabs  5220  pwnss  5226  difelpw  5228  rabelpw  5229  0inp0  5235  copsexgw  5358  copsexg  5359  euotd  5381  elopab  5393  elvvuni  5610  posn  5619  frsn  5621  eqrelriv  5644  relsnb  5657  relopabiALT  5678  opabid2  5683  ididg  5707  iss  5888  ord0eln0  6245  sucidg  6269  nsuceq0  6271  funopg  6392  fn0  6487  f00  6579  f0bi  6580  f10d  6672  f1o00  6673  fo00  6674  brprcneu  6686  fvprc  6687  dffn5  6749  fsn  6928  funop  6942  funsndifnop  6944  fnsnb  6959  eufnfv  7023  f1eqcocnv  7089  f1eqcocnvOLD  7090  nfriotadw  7156  nfriotad  7160  riotaprop  7176  oprabidw  7222  oprabid  7223  elrnmpo  7324  ov6g  7350  ovelrn  7362  caovmo  7423  offn  7459  caofinvl  7476  fr3nr  7535  onprc  7540  ordeleqon  7544  onint0  7553  0elsuc  7592  onuninsuci  7597  orduninsuc  7600  ordzsl  7602  onzsl  7603  tfinds  7616  limomss  7627  limom  7638  peano5  7649  peano5OLD  7650  xpexr  7674  eqop2  7782  opreuopreu  7784  1stconst  7846  2ndconst  7847  funsssuppss  7910  dftpos3  7964  dftpos4  7965  wfrlem4  8036  wfrlem14  8046  oawordeulem  8260  omwordi  8277  nnmwordi  8341  riiner  8450  ecopover  8481  map0g  8543  mapsnd  8545  elixpsn  8596  en0  8669  en0OLD  8670  en0ALT  8671  en1  8676  en1OLD  8677  fiprc  8700  sbthlem2  8735  sbthlem4  8737  sbthlem5  8738  nneneq  8807  findcard  8819  findcard2  8820  sdom1  8854  fineqvlem  8868  nfielex  8881  findcard2OLD  8891  elfiun  9024  marypha1lem  9027  oicl  9123  oif  9124  oion  9130  hartogslem1  9136  hartogs  9138  wemapso2  9147  card2on  9148  0wdom  9164  brwdom2  9167  inf3lem6  9226  cantnflem3  9284  cantnflem4  9285  wemapwe  9290  cnfcom  9293  tctr  9334  r1tr  9357  r1rankidb  9385  r1pw  9426  scottex  9466  scott0  9467  bnd2  9474  eldju2ndl  9505  tskwe  9531  oncard  9541  cardlim  9553  harsdom  9576  en2eleq  9587  dfac8alem  9608  cardaleph  9668  iunfictbso  9693  infmap2  9797  ackbij1lem18  9816  cff  9827  cfsuc  9836  cff1  9837  cflim2  9842  cfss  9844  sdom2en01  9881  infpssrlem4  9885  fin23lem7  9895  fin23lem11  9896  isfin2-2  9898  fin23lem26  9904  fin23lem19  9915  fin23lem17  9917  isf34lem2  9952  isf34lem4  9956  fin1a2lem6  9984  fin1a2lem10  9988  fin1a2lem12  9990  itunifn  9996  hsmexlem1  10005  axcc2lem  10015  dcomex  10026  axdc3lem4  10032  ondomon  10142  konigthlem  10147  pwcfsdom  10162  cfpwsdom  10163  axpowndlem3  10178  canth4  10226  canthnumlem  10227  canthwelem  10229  canthwe  10230  canthp1lem2  10232  pwfseqlem4  10241  pwfseqlem5  10242  gchaleph  10250  gch2  10254  winainflem  10272  0tsk  10334  rankcf  10356  tskcard  10360  gruina  10397  grutsk  10401  tskmid  10419  indpi  10486  nqereu  10508  mulcanenq  10539  recmulnq  10543  archnq  10559  ltsopr  10611  1ne0sr  10675  0idsr  10676  00sr  10678  leid  10893  lelttric  10904  divcan3  11481  lemul1a  11651  nn1suc  11817  nn0n0n1ge2b  12123  xnn0xr  12132  xnn0nemnf  12138  nn0lt10b  12204  nn0ind-raph  12242  elnn1uz2  12486  indstr2  12488  uzsupss  12501  rpnnen1lem4  12541  rpnnen1lem5  12542  xrnemnf  12674  xrnepnf  12675  mnfltxr  12684  xnn0n0n1ge2b  12688  xnn0ge0  12690  xrlttri  12694  xrlttr  12695  xrleid  12706  qbtwnxr  12755  xmullem2  12820  xlemul1a  12843  xrub  12867  reltxrnmnf  12897  ixxun  12916  xnn0xrge0  13059  fztpval  13139  fseq1p1m1  13151  elfznelfzob  13313  ltweuz  13499  fzfi  13510  fsuppmapnn0fiubex  13530  ser0f  13594  0exp  13635  faclbnd4lem1  13824  bcn1  13844  hashnemnf  13875  hashv01gt1  13876  hashsnle1  13949  hashgt12el2  13955  hashpw  13968  hashf1  13988  fz1isolem  13992  hash2prb  14003  0wrd0  14060  wrdlen1  14074  ccatvalfn  14103  eqs1  14134  wrdl1exs1  14135  swrdlen  14177  swrdwrdsymb  14192  swrdspsleq  14195  cats1un  14251  wrdind  14252  wrd2ind  14253  swrdccatin1  14255  repswsymballbi  14310  cshw1  14352  scshwfzeqfzo  14356  wrdl2exs2  14476  trclfvcotr  14537  relexp1g  14554  relexp0rel  14565  relexprelg  14566  relexpreld  14568  sqr0lem  14769  sqrtsq  14798  mptfzshft  15305  prodf1f  15419  egt2lt3  15730  0dvds  15801  nn0onn  15904  nn0o  15907  divalgmod  15930  flodddiv4  15937  bitsp1o  15955  gcddvds  16025  bezout  16066  lcmdvds  16128  rpdvds  16180  1nprm  16199  prmind2  16205  nnoddn2prmb  16329  pcpre1  16358  vdwapf  16488  vdwapid1  16491  ram0  16538  ramz  16541  prmolefac  16562  cshws0  16618  prmlem0  16622  strle1  16776  restsspw  16890  prdsdsfn  16924  imasdsfn  16973  imasaddfnlem  16987  imasvscafn  16996  xpsfrnel  17021  isacs1i  17114  cidfn  17136  fnhomeqhomf  17148  comffn  17162  isoval  17224  sscres  17282  cofucl  17348  idffth  17394  ressffth  17399  cat1lem  17556  catcoppccl  17577  catcoppcclOLD  17578  estrchomfn  17596  funcestrcsetclem4  17604  funcestrcsetclem7  17607  equivestrcsetc  17613  funcsetcestrclem4  17619  funcsetcestrclem7  17622  1stfcl  17658  2ndfcl  17659  prfcl  17664  evlfcl  17684  curf1cl  17690  curfcl  17694  hofcl  17721  yonedainv  17743  pospo  17805  lubfun  17812  glbfun  17825  joindmss  17839  meetdmss  17853  ipopos  17996  acsficl2d  18012  dirref  18061  mgmidcl  18092  mgmlrid  18093  ielefmnd  18268  smndex1basss  18286  smndex1n0mnd  18293  cntzssv  18676  idresperm  18732  symgvalstruct  18743  pmtrfmvdn0  18808  symggen  18816  psgnunilem1  18839  psgnprfval  18867  slwpgp  18956  frgpmhm  19109  frgpuptinv  19115  frgpup3lem  19121  gsumzoppg  19283  gsumcom2  19314  abv0  19821  rrgsupp  20283  zrhrhm  20432  psgnodpmr  20506  frlmphllem  20696  frlmphl  20697  ellspd  20718  psrvscafval  20869  psrridm  20883  ltbwe  20955  psrbag0  20974  psrbagsn  20975  subrgascl  20978  mattpostpos  21305  mavmul0  21403  mavmul0g  21404  mdet0f1o  21444  m1detdiag  21448  m2detleiblem5  21476  m2detleiblem6  21477  m2detleiblem3  21480  m2detleiblem4  21481  maducoeval2  21491  d1mat2pmat  21590  chpmat1dlem  21686  chpmat1d  21687  baspartn  21805  eltg3  21813  topnex  21847  fctop  21855  cctop  21857  discld  21940  mretopd  21943  neipeltop  21980  neitr  22031  restcls  22032  ordtbaslem  22039  ordtuni  22041  idcn  22108  cnrmi  22211  cmpsublem  22250  cmpsub  22251  tgcmp  22252  uncmp  22254  hauscmplem  22257  cmpfi  22259  bwth  22261  1stcrestlem  22303  disllycmp  22349  dis1stc  22350  refref  22364  kgeni  22388  1stckgenlem  22404  kqffn  22576  snfil  22715  filconn  22734  cfinfil  22744  ufileu  22770  filufint  22771  fixufil  22773  cfinufil  22779  ufilen  22781  fin1aufil  22783  fmf  22796  rnelfm  22804  flimclslem  22835  hauspwpwf1  22838  supnfcls  22871  flimfnfcls  22879  fclscmp  22881  alexsubALTlem2  22899  alexsubALTlem3  22900  alexsubALT  22902  ptcmplem1  22903  cnextrel  22914  tsmsfbas  22979  ustref  23070  trust  23081  restutop  23089  isusp  23113  xmet0  23194  imasdsf1olem  23225  blfvalps  23235  blfps  23258  blf  23259  restmetu  23422  dscmet  23424  isngp2  23449  nm0  23481  nrginvrcn  23544  nmoix  23581  qdensere  23621  iccconn  23681  iccpnfcnv  23795  xrhmeo  23797  lebnumlem3  23814  metsscmetcld  24166  bcthlem5  24179  csschl  24227  rrxmfval  24257  minveclem3b  24279  cniccbdd  24312  ovolicc2lem4  24371  iunmbl  24404  ioorinv  24427  ioorcl  24428  i1f1lem  24540  limcvallem  24722  ellimc2  24728  limccnp  24742  limccnp2  24743  limcco  24744  perfdvf  24754  recnprss  24755  fncpn  24784  dvcmulf  24796  c1lip1  24848  lhop2  24866  q1pcl  25007  r1pdeglt  25010  ply1remlem  25014  plyssc  25048  ulm0  25237  cxpeq0  25520  cxplea  25538  cxplogb  25623  asinlem  25705  isppw2  25951  muval2  25970  dchrfi  26090  dchrpt  26102  bposlem6  26124  lgsdir2lem2  26161  lgsqr  26186  gausslemma2dlem4  26204  2lgslem2  26230  2lgslem3  26239  2lgs  26242  2sqlem7  26259  2sqlem11  26264  chtppilim  26310  tgldimor  26547  tgcgr4  26576  tglnfn  26592  tglnunirn  26593  mirne  26712  mircinv  26713  perpln1  26755  perpln2  26756  lmiisolem  26841  xmstrkgc  26931  axcgrtr  26960  axsegconlem9  26970  axlowdimlem5  26991  axlowdimlem17  27003  axlowdim1  27004  uhgr0e  27116  edglnl  27188  uhgr0edgfi  27282  issubgr2  27314  subgrprop2  27316  egrsubgr  27319  0grsubgr  27320  0uhgrsubgr  27321  uhgrsubgrself  27322  nbgr0vtx  27398  nbgr1vtx  27400  nbgrssovtx  27403  nb3grprlem1  27422  uvtx01vtx  27439  cplgr1vlem  27471  cplgr1v  27472  usgrexilem  27482  wlkcomp  27672  wlk1walk  27680  wlkp1lem5  27719  uhgrwkspthlem1  27794  pthdlem1  27807  clwlkcomp  27820  lfgrn1cycl  27843  uspgrn2crct  27846  wwlksn0s  27899  umgrwwlks2on  27995  clwwlkn  28063  clwwlkn1  28078  0ewlk  28151  1ewlk  28152  0spth  28163  upgr1wlkdlem2  28183  wlk2v2e  28194  upgr3v3e3cycl  28217  upgr4cycl4dv4e  28222  eupth0  28251  frgr0v  28299  frgr1v  28308  1vwmgr  28313  ex-opab  28469  grpoinvf  28567  nvmid  28694  nmlnoubi  28831  hiidrcl  29130  hsn0elch  29283  shjshseli  29528  cmbr4i  29636  dfiop2  29788  kbpj  29991  nmopun  30049  adjeq0  30126  kbass2  30152  pjssdif1i  30210  pjinvari  30226  pjcmul2i  30237  pj3i  30243  stge1i  30273  stle0i  30274  sumdmdlem2  30454  dmdbr6ati  30458  dmdbr7ati  30459  rabsnel  30520  unidifsnel  30556  unidifsnne  30557  disjdifprg  30587  ofoprabco  30675  padct  30728  fpwrelmapffslem  30741  xrlelttric  30749  xnn0gt0  30766  iundisj2cnt  30794  f1ocnt  30797  fz1nnct  30798  fz1nntr  30799  hashxpe  30801  dvdszzq  30803  nn0min  30808  wrdt2ind  30899  xrge0tsmsbi  30991  locfinref  31459  dispcmp  31477  zartopn  31493  zarcmplem  31499  pstmxmet  31515  xrge0iifcnv  31551  xrge0iif1  31556  qqhre  31636  esumcl  31664  esumpr2  31701  esumpinfval  31707  esumpcvgval  31712  ofcfn  31734  pwsiga  31764  prsiga  31765  sigainb  31770  ldgenpisyslem1  31797  measiuns  31851  relfae  31881  pmeasmono  31957  sitgf  31980  eulerpartgbij  32005  sgnmulsgn  32182  sgnmulsgp  32183  signswch  32206  signslema  32207  signstlen  32212  signstfvn  32214  circlevma  32288  bnj216  32377  bnj151  32524  bnj517  32532  bnj970  32594  bnj1145  32640  bnj1498  32708  fineqvrep  32731  fineqvac  32733  0nn0m1nnn0  32738  pthhashvtx  32756  acycgr0v  32777  prclisacycgr  32780  umgracycusgr  32783  cusgracyclt3v  32785  subfacp1lem5  32813  erdszelem8  32827  kur14lem1  32835  indispconn  32863  cvmsss2  32903  satfvsuclem2  32989  satfrel  32996  satfrnmapom  32999  satfv0fun  33000  satf00  33003  satf0suclem  33004  fmlasuc0  33013  msubrn  33158  dfpo2  33392  dfon2lem7  33435  frxp2  33471  frxp3  33477  nosgnn0i  33548  nolesgn2ores  33561  nogesgn1ores  33563  nosepnelem  33568  nosepdmlem  33572  nosupbnd1lem3  33599  nosupbnd1lem5  33601  nosupbnd2lem1  33604  noinfbnd1lem3  33614  noinfbnd1lem5  33616  noinfbnd2lem1  33619  oldval  33724  made0  33743  lrrecpo  33784  brbigcup  33886  elsingles  33906  fnimage  33917  funpartlem  33930  dfrdg4  33939  imagesset  33941  altopthsn  33949  elaltxp  33963  ellines  34140  linethru  34141  rankeq1o  34159  elhf2  34163  hfninf  34174  nn0prpwlem  34197  fneref  34225  neibastop2lem  34235  limsucncmpi  34320  bj-exlimmpbir  34786  curryset  34821  bj-snglex  34849  bj-restpw  34947  bj-inftyexpidisj  35065  topdifinffinlem  35204  relowlssretop  35220  rdgeqoa  35227  finxpreclem6  35253  fvineqsneq  35269  pibt2  35274  poimirlem23  35486  poimirlem29  35492  poimirlem31  35494  volsupnfl  35508  cnambfre  35511  dvasin  35547  dvacos  35548  sdclem2  35586  sstotbnd2  35618  ssbnd  35632  ismgmOLD  35694  grpokerinj  35737  rngomndo  35779  isdrngo1  35800  ac6s6  36016  iss2  36165  cnvelrels  36299  cosselrels  36300  brssrid  36306  brcnvssrid  36311  dfdisjs5  36509  eldisjs5  36523  prtlem12  36567  riotasv2d  36657  lkrscss  36798  islshpkrN  36820  isline  37439  ispointN  37442  0psubN  37449  linepsubN  37452  atpsubN  37453  cdlemk36  38613  diafn  38734  dibfna  38854  dibvalrel  38863  dicvalrelN  38885  diclspsn  38894  dihvalrel  38979  dih1  38986  lclkrlem1  39206  lclkr  39233  mapd1o  39348  mapdin  39362  hdmapfnN  39529  hgmapfnN  39588  lcmineqlem10  39729  sticksstones9  39779  repncan2  40014  sn-inelr  40084  elrfirn  40161  ismrcd1  40164  istopclsd  40166  rabren3dioph  40281  jm2.17b  40427  jm2.22  40461  jm2.23  40462  ttac  40502  pw2f1ocnv  40503  dnnumch1  40513  hbtlem5  40597  mncn0  40608  aaitgo  40631  rngunsnply  40642  ensucne0OLD  40763  clcnvlem  40848  relexp01min  40939  ntrf  41351  ssrecnpr  41540  seff  41541  sblpnf  41542  nzss  41549  dvconstbi  41566  ipo0  41681  ifr0  41682  addrfn  41704  subrfn  41705  mulvfn  41706  refsum2cnlem1  42194  ellimciota  42773  dvmptconst  43074  dvmptidg  43076  dvmulcncf  43084  dvdivcncf  43086  stoweidlem26  43185  stoweidlem50  43209  stoweidlem57  43216  aiotaval  44202  ndfatafv2nrn  44328  afv2ndefb  44331  funop1  44390  fun2dmnopgexmpl  44391  2ffzoeq  44436  iccpartiltu  44490  iccpartigtl  44491  zofldiv2ALTV  44730  evenprm2  44782  9fppr8  44805  stgoldbwt  44844  nnsum3primesle9  44862  nnsum4primeseven  44868  nnsum4primesevenALTV  44869  tgblthelfgott  44883  isomgreqve  44893  uspgrex  44928  0mgm  44944  nnsgrpmgm  44986  c0snmhm  45089  rngchomffvalALTV  45169  funcringcsetcALTV2lem4  45213  funcringcsetclem4ALTV  45236  srhmsubc  45250  rhmsubclem1  45260  srhmsubcALTV  45268  rhmsubcALTVlem1  45278  mapsnop  45296  zlmodzxzldeplem4  45460  zofldiv2  45493  fdivval  45501  nnlog2ge0lt1  45528  dig1  45570  itcoval2  45626  itcoval3  45627  mosn  45774  mo0  45775  mof02  45782  mofeu  45791  f102g  45795  f1mo  45796  f1omo  45804  intubeu  45886  unilbeu  45887  functhinclem1  45938  fullthinc  45943  thincciso  45946  indthinc  45949  indthincALT  45950