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  1099  spei  2425  nfald2  2476  nfabd2  2947  raleleq  3333  ceqsexv2d  3502  dedhb  3664  csbie2df  4404  ssdifeq0  4445  dedth  4544  pwidgOLD  4581  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  4830  unimax  4908  intmin3  4939  eqbrtrdi  5148  al0ssb  5269  vneqv  5277  rabelpw  5305  intabs  5317  difelpw  5322  0inp0  5327  axpr  5396  intidg  5436  copsexgw  5470  copsexgwOLD  5471  copsexg  5472  euotd  5494  elopab  5509  elvvuni  5736  posn  5745  frsn  5747  eqrelriv  5773  relsnb  5787  relopabiALT  5808  opabid2  5813  ididg  5837  iss  6035  dfpo2  6298  ord0eln0  6418  sucidg  6445  nsuceq0  6447  funopg  6571  fn0  6667  f00  6761  f0bi  6762  f10d  6856  f1o00  6857  fo00  6858  brprcneu  6872  brprcneuALT  6873  dffn5  6940  fsn  7132  funop  7149  funsndifnop  7151  fnsnbOLD  7167  eufnfv  7231  f1ounsn  7276  f1eqcocnv  7305  nfriotadw  7381  nfriotad  7384  riotaprop  7400  oprabidw  7447  oprabid  7448  elrnmpo  7552  ov6g  7580  ovelrn  7593  caovmo  7654  offn  7694  caofinvl  7713  fr3nr  7774  onprc  7780  ordeleqon  7784  onint0  7793  0elsuc  7834  onuninsuci  7839  orduninsuc  7842  ordzsl  7844  onzsl  7845  tfinds  7859  limomss  7870  limom  7881  peano5  7893  xpexr  7918  eqop2  8032  opreuopreu  8034  1stconst  8100  2ndconst  8101  frxp2  8145  frxp3  8152  funsssuppss  8191  dftpos3  8245  dftpos4  8246  oawordeulem  8544  omwordi  8561  nnmwordi  8626  riiner  8793  ecopover  8824  map0g  8894  mapsnd  8896  elixpsn  8947  en0  9027  en0ALT  9028  en0r  9029  en1  9033  snfi  9053  fiprc  9054  sbthlem2  9089  sbthlem4  9091  sbthlem5  9092  0domg  9105  findcard  9161  findcard2  9162  nneneq  9203  sdom1  9223  1sdom2dom  9227  fineqvlem  9239  nfielex  9247  enp1i  9252  elfiun  9403  marypha1lem  9406  oicl  9504  oif  9505  oion  9511  hartogslem1  9517  hartogs  9519  wemapso2  9528  card2on  9529  0wdom  9545  brwdom2  9548  elirrv  9572  inf3lem6  9615  cantnflem3  9673  cantnflem4  9674  wemapwe  9679  cnfcom  9682  ssttrcl  9697  ttrclselem2  9708  tctr  9720  r1tr  9761  r1rankidb  9789  r1pw  9830  scottex  9875  scottexOLD  9876  scott0b  9879  scott0OLD  9880  bnd2  9898  eldju2ndl  9932  tskwe  9958  oncard  9968  cardlim  9980  harsdom  10003  en2eleq  10014  dfac8alem  10035  dfac8b  10037  cardaleph  10095  iunfictbso  10120  infmap2  10222  ackbij1lem18  10241  cff  10252  cfsuc  10262  cff1  10263  cflim2  10268  cfss  10270  sdom2en01  10307  infpssrlem4  10311  fin23lem7  10321  fin23lem11  10322  isfin2-2  10324  fin23lem26  10330  fin23lem19  10341  fin23lem17  10343  isf34lem2  10378  isf34lem4  10382  fin1a2lem6  10410  fin1a2lem10  10414  fin1a2lem12  10416  itunifn  10422  hsmexlem1  10431  axcc2lem  10441  dcomex  10452  axdc3lem4  10458  ondomon  10574  konigthlem  10580  pwcfsdom  10595  cfpwsdom  10596  axpowndlem3  10611  canth4  10659  canthnumlem  10660  canthwelem  10662  canthwe  10663  canthp1lem2  10665  pwfseqlem4  10674  pwfseqlem5  10675  gchaleph  10683  gch2  10687  winainflem  10705  0tsk  10767  rankcf  10789  tskcard  10793  gruina  10830  grutsk  10834  tskmid  10852  indpi  10919  nqereu  10941  mulcanenq  10972  recmulnq  10976  archnq  10992  ltsopr  11044  1ne0sr  11108  0idsr  11109  00sr  11111  leid  11333  lelttric  11344  divcan3  11925  divid  11929  div0  11930  lemul1a  12096  nn1suc  12282  nn0n0n1ge2b  12600  xnn0xr  12609  xnn0nemnf  12615  0nn0m1nnn0  12678  nn0lt10b  12686  nn0ind-raph  12724  elnn1uz2  12977  indstr2  12979  uzsupss  12992  rpnnen1lem4  13032  rpnnen1lem5  13033  xrnemnf  13170  xrnepnf  13171  mnfltxr  13180  xnn0n0n1ge2b  13185  xnn0ge0  13187  xrlttri  13192  xrlttr  13193  xrleid  13204  qbtwnxr  13254  xmullem2  13319  xlemul1a  13342  xrub  13366  reltxrnmnf  13397  ixxun  13416  xnn0xrge0  13561  fztpval  13643  fseq1p1m1  13655  elfznelfzob  13832  ltweuz  14027  fzfi  14038  fsuppmapnn0fiubex  14058  ser0f  14121  0exp  14163  faclbnd4lem1  14359  bcn1  14379  hashnemnf  14410  hashv01gt1  14411  hashsnle1  14484  hashgt12el2  14490  hashpw  14503  hashf1  14524  fz1isolem  14528  hash2prb  14539  hash3tpb  14562  0wrd0  14607  wrdlen1  14621  ccatvalfn  14648  eqs1  14682  wrdl1exs1  14683  swrdlen  14717  swrdwrdsymb  14734  swrdspsleq  14737  cats1un  14792  wrdind  14793  wrd2ind  14794  swrdccatin1  14796  repswsymballbi  14853  cshw1  14895  scshwfzeqfzo  14899  wrdl2exs2  15019  trclfvcotr  15084  relexp1g  15101  relexp0rel  15112  relexprelg  15113  relexpreld  15115  sgnmulsgn  15184  sqrt0  15330  sqrtsq  15358  mptfzshft  15866  prodf1f  15983  egt2lt3  16298  0dvds  16370  nn0onn  16474  nn0o  16477  divalgmod  16500  flodddiv4  16509  bitsp1o  16527  gcddvds  16597  bezout  16637  lcmdvds  16702  rpdvds  16754  1nprm  16773  prmind2  16779  dvdszzq  16816  nnoddn2prmb  16909  pcpre1  16938  vdwapf  17068  vdwapid1  17071  ram0  17118  ramz  17121  prmolefac  17142  cshws0  17197  prmlem0  17201  strle1  17254  restsspw  17520  prdsdsfn  17554  imasdsfn  17604  imasaddfnlem  17618  imasvscafn  17627  xpsfrnel  17652  isacs1i  17749  cidfn  17771  fnhomeqhomf  17783  comffn  17797  isoval  17858  sscres  17916  cofucl  17981  idffth  18028  ressffth  18033  cat1lem  18189  catcoppccl  18210  estrchomfn  18227  funcestrcsetclem4  18235  funcestrcsetclem7  18238  equivestrcsetc  18244  funcsetcestrclem4  18250  funcsetcestrclem7  18253  1stfcl  18289  2ndfcl  18290  prfcl  18295  evlfcl  18314  curf1cl  18320  curfcl  18324  hofcl  18351  yonedainv  18373  pospo  18435  lubfun  18442  glbfun  18455  joindmss  18469  meetdmss  18483  ipopos  18628  acsficl2d  18644  dirref  18693  mgmidcl  18763  mgmlrid  18764  ielefmnd  19000  smndex1basss  19021  smndex1n0mnd  19028  degenmgm  19054  degenmgm2  19057  cntzssv  19459  idresperm  19517  symgvalstruct  19528  pmtrfmvdn0  19593  symggen  19601  psgnunilem1  19624  psgnprfval  19652  slwpgp  19744  frgpmhm  19896  frgpuptinv  19902  frgpup3lem  19908  gsumzoppg  20075  gsumcom2  20106  c0snmhm  20608  srhmsubc  20846  rhmsubclem1  20851  rrgsupp  20867  abv0  20993  zrhrhm  21728  psgnodpmr  21807  frlmphllem  21997  ellspd  22019  psrvscafval  22167  psrridm  22181  ltbwe  22264  psrbag0  22282  psrbagsn  22283  subrgascl  22286  psdmul  22398  mattpostpos  22680  mavmul0  22778  mavmul0g  22779  mdet0f1o  22819  m1detdiag  22823  m2detleiblem5  22851  m2detleiblem6  22852  m2detleiblem3  22855  m2detleiblem4  22856  maducoeval2  22866  d1mat2pmat  22968  chpmat1dlem  23064  chpmat1d  23065  baspartn  23183  eltg3  23191  topnex  23225  fctop  23233  cctop  23235  discld  23318  mretopd  23321  neipeltop  23358  neitr  23409  restcls  23410  ordtbaslem  23417  ordtuni  23419  idcn  23486  cnrmi  23589  cmpsublem  23628  cmpsub  23629  tgcmp  23630  uncmp  23632  hauscmplem  23635  cmpfi  23637  bwth  23639  1stcrestlem  23681  disllycmp  23728  dis1stc  23729  refref  23743  kgeni  23767  1stckgenlem  23783  kqffn  23955  snfil  24094  filconn  24113  cfinfil  24123  ufileu  24149  filufint  24150  fixufil  24152  cfinufil  24158  ufilen  24160  fin1aufil  24162  fmf  24175  rnelfm  24183  flimclslem  24214  hauspwpwf1  24217  supnfcls  24250  flimfnfcls  24258  fclscmp  24260  alexsubALTlem2  24278  alexsubALTlem3  24279  alexsubALT  24281  ptcmplem1  24282  cnextrel  24293  tsmsfbas  24358  ustref  24449  trust  24459  restutop  24467  isusp  24491  xmet0  24572  imasdsf1olem  24603  blfvalps  24613  blfps  24636  blf  24637  restmetu  24800  dscmet  24802  isngp2  24827  nm0  24859  nrginvrcn  24922  nmoix  24959  qdensere  24999  iccconn  25061  iccpnfcnv  25176  xrhmeo  25178  lebnumlem3  25195  metsscmetcld  25547  bcthlem5  25560  csschl  25608  rrxmfval  25638  minveclem3b  25660  cniccbdd  25693  ovolicc2lem4  25752  iunmbl  25785  ioorinv  25808  ioorcl  25809  i1f1lem  25921  limcvallem  26103  ellimc2  26109  limccnp  26123  limccnp2  26124  limcco  26125  perfdvf  26135  recnprss  26136  fncpn  26165  dvcmulf  26177  c1lip1  26229  lhop2  26247  q1pcl  26387  r1pdeglt  26390  ply1remlem  26395  plyssc  26430  ulm0  26627  cxpeq0  26916  cxplea  26934  cxplogb  27024  asinlem  27106  isppw2  27352  muval2  27371  dchrfi  27492  dchrpt  27504  bposlem6  27526  lgsdir2lem2  27563  lgsqr  27588  gausslemma2dlem4  27606  2lgslem2  27632  2lgslem3  27641  2lgs  27644  2sqlem7  27661  2sqlem11  27666  chtppilim  27712  nosgnn0i  27896  nolesgn2ores  27909  nogesgn1ores  27911  nosepnelem  27916  nosepdmlem  27920  nosupbnd1lem3  27947  nosupbnd1lem5  27949  nosupbnd2lem1  27952  noinfbnd1lem3  27962  noinfbnd1lem5  27964  noinfbnd2lem1  27967  oldval  28100  made0  28129  lrrecpo  28207  pncan2s  28340  divscan3d  28502  abssor  28512  om2noseqfo  28564  noseqrdglem  28571  noseqrdgfn  28572  noseqrdg0  28573  onsfi  28622  nohalf  28690  expsne0  28702  pw2divscan3d  28707  tgldimor  28845  tgcgr4  28874  tglnfn  28890  tglnunirn  28891  mirne  29019  mircinv  29020  perpln1  29065  perpln2  29066  tgplnfn  29133  lmiisolem  29181  prlngmid2  29319  xmstrkgc  29343  axcgrtr  29373  axsegconlem9  29383  axlowdimlem5  29404  axlowdimlem17  29416  axlowdim1  29417  uhgr0e  29529  edglnl  29601  uhgr0edgfi  29701  issubgr2  29733  subgrprop2  29735  egrsubgr  29738  0grsubgr  29739  0uhgrsubgr  29740  uhgrsubgrself  29741  nbgr1vtx  29819  nbgrssovtx  29822  nb3grprlem1  29841  uvtx01vtx  29858  cplgr1vlem  29890  cplgr1v  29891  usgrexilem  29901  wlkcomp  30091  wlk1walk  30099  wlkp1lem5  30136  pthhashvtx  30195  uhgrwkspthlem1  30219  pthdlem1  30232  clwlkcomp  30246  lfgrn1cycl  30274  uspgrn2crct  30277  wwlksn0s  30330  usgrwwlks2on  30427  umgrwwlks2on  30428  clwwlkn  30497  clwwlkn1  30512  0ewlk  30585  1ewlk  30586  0spth  30597  upgr1wlkdlem2  30617  wlk2v2e  30638  upgr3v3e3cycl  30661  upgr4cycl4dv4e  30666  eupth0  30695  frgr0v  30743  frgr1v  30752  1vwmgr  30757  ex-opab  30913  grpoinvf  31014  nvmid  31141  nmlnoubi  31278  hiidrcl  31577  hsn0elch  31730  shjshseli  31975  cmbr4i  32083  dfiop2  32235  kbpj  32438  nmopun  32496  adjeq0  32573  kbass2  32599  pjssdif1i  32657  pjinvari  32673  pjcmul2i  32684  pj3i  32690  stge1i  32720  stle0i  32721  sumdmdlem2  32901  dmdbr6ati  32905  dmdbr7ati  32906  rabsnel  32976  unidifsnel  33011  unidifsnne  33012  disjdifprg  33050  ofoprabco  33139  padct  33191  fpwrelmapffslem  33205  nn0mnfxrd  33224  xrlelttric  33225  xnn0gt0  33242  iundisj2cnt  33272  f1ocnt  33273  fz1nnct  33274  fz1nntr  33275  hashxpe  33280  nn0min  33293  sgnmulsgp  33304  wrdt2ind  33397  xrge0tsmsbi  33516  opprabs  33886  rtelextdg2lem  34238  2sqr3minply  34292  locfinref  34353  dispcmp  34371  zartopn  34387  zarcmplem  34393  pstmxmet  34409  xrge0iifcnv  34445  xrge0iif1  34450  qqhre  34532  esumcl  34542  esumpr2  34579  esumpinfval  34585  esumpcvgval  34590  ofcfn  34612  pwsiga  34642  prsiga  34643  sigainb  34649  ldgenpisyslem1  34676  measiuns  34730  relfae  34760  pmeasmono  34837  sitgf  34860  eulerpartgbij  34885  signswch  35071  signslema  35072  signstlen  35077  signstfvn  35079  circlevma  35152  bnj216  35244  bnj151  35388  bnj517  35396  bnj970  35458  bnj1145  35504  bnj1498  35572  r1omhfb  35624  rankscottu  35638  fineqvrep  35642  fineqvac  35644  fineqvnttrclselem1  35649  fineqvnttrclselem2  35650  fineqvnttrclse  35652  fineqvinfep  35653  r1omhfbregs  35665  kard0b  35687  rankkardu  35699  wevgblacfn  35710  vonf1osev  35711  acycgr0v  35729  prclisacycgr  35732  umgracycusgr  35735  cusgracyclt3v  35737  subfacp1lem5  35765  erdszelem8  35779  kur14lem1  35787  indispconn  35815  cvmsss2  35855  satfvsuclem2  35941  satfrel  35948  satfrnmapom  35951  satfv0fun  35952  satf00  35955  satf0suclem  35956  fmlasuc0  35965  msubrn  36110  dfon2lem7  36368  brbigcup  36477  elsingles  36497  fnimage  36508  funpartlem  36523  dfrdg4  36532  imagesset  36534  altopthsn  36543  elaltxp  36557  ellines  36734  linethru  36735  rankeq1o  36753  elhf2  36757  hfninf  36768  nn0prpwlem  36943  fneref  36971  neibastop2lem  36981  limsucncmpi  37066  tz9.1tco  37104  bj-exlimmpbir  37659  curryset  37692  bj-snglex  37719  bj-axnul  37819  bj-restpw  37844  bj-inftyexpidisj  37964  topdifinffinlem  38103  relowlssretop  38119  rdgeqoa  38126  finxpreclem6  38152  fvineqsneq  38168  pibt2  38173  poimirlem23  38394  poimirlem29  38400  poimirlem31  38402  volsupnfl  38416  cnambfre  38419  dvasin  38455  dvacos  38456  sdclem2  38494  sstotbnd2  38526  ssbnd  38540  ismgmOLD  38602  grpokerinj  38645  rngomndo  38687  isdrngo1  38708  ac6s6  38922  iss2  39094  relecxrn  39157  sucmapsuc  39239  cosselrels  39325  cnvelrels  39326  brssrid  39332  brcnvssrid  39337  dfdisjs5  39547  eldisjs5  39573  eldisjsim3  39687  mpets2  39705  pets  39716  prtlem12  39742  riotasv2d  39832  lkrscss  39973  islshpkrN  39995  isline  40614  ispointN  40617  0psubN  40624  linepsubN  40627  atpsubN  40628  cdlemk36  41788  diafn  41909  dibfna  42029  dibvalrel  42038  dicvalrelN  42060  diclspsn  42069  dihvalrel  42154  dih1  42161  lclkrlem1  42381  lclkr  42408  mapd1o  42523  mapdin  42537  hdmapfnN  42704  hgmapfnN  42763  lcmineqlem10  42906  sticksstones9  43022  sn-iotalem  43093  readvrec2  43238  readvrec  43239  repncan2  43259  elrfirn  43542  ismrcd1  43545  istopclsd  43547  rabren3dioph  43658  jm2.17b  43804  jm2.22  43838  jm2.23  43839  ttac  43879  pw2f1ocnv  43880  dnnumch1  43887  hbtlem5  43971  mncn0  43982  aaitgo  44005  rngunsnply  44012  unielss  44061  onexlimgt  44086  cantnfresb  44167  dflim5  44172  naddwordnexlem4  44244  safesnsupfiss  44257  safesnsupfidom1o  44259  safesnsupfilb  44260  ensucne0OLD  44372  clcnvlem  44465  relexp01min  44555  ntrf  44965  ssrecnpr  45134  seff  45135  sblpnf  45136  nzss  45143  dvconstbi  45160  ipo0  45274  ifr0  45275  addrfn  45296  subrfn  45297  mulvfn  45298  wfaxrep  45819  refsum2cnlem1  45873  rn1st  46104  ellimciota  46446  dvmptconst  46745  dvmptidg  46747  dvmulcncf  46755  dvdivcncf  46757  stoweidlem26  46856  stoweidlem50  46880  stoweidlem57  46887  tannpoly  47760  tmachlem-agreefin  47778  aiotaval  47985  ndfatafv2nrn  48111  afv2ndefb  48114  funop1  48173  fun2dmnopgexmpl  48174  2ffzoeq  48218  2ltceilhalf  48222  m1modne  48244  iccpartiltu  48324  iccpartigtl  48325  zofldiv2ALTV  48580  evenprm2  48632  9fppr8  48655  stgoldbwt  48694  nnsum3primesle9  48712  nnsum4primeseven  48718  nnsum4primesevenALTV  48719  tgblthelfgott  48733  dfclnbgr6  48774  cycl3grtri  48865  grtrimap  48866  stgredgel  48875  stgr1  48879  isubgr3stgrlem2  48885  isubgr3stgrlem3  48886  usgrexmpl2trifr  48955  gpg5nbgrvtx13starlem1  48989  gpg5nbgrvtx13starlem2  48990  gpg5nbgrvtx13starlem3  48991  gpg5nbgr3star  48999  gpg3kgrtriex  49007  uspgrex  49068  0mgm  49083  nnsgrpmgm  49093  rngchomffvalALTV  49195  rhmsubcALTVlem1  49198  funcringcsetcALTV2lem4  49210  funcringcsetclem4ALTV  49233  srhmsubcALTV  49242  mapsnop  49276  zlmodzxzldeplem4  49435  zofldiv2  49463  fdivval  49471  nnlog2ge0lt1  49498  dig1  49540  itcoval2  49596  itcoval3  49597  mosn  49743  mo0  49744  mof02  49769  mofeu  49778  f102g  49782  f1mo  49783  tposres0  49805  f1omo  49821  f1omoOLD  49822  resipos  49903  intubeu  49912  unilbeu  49913  sectfn  49957  nelsubclem  49995  idfu1stf1o  50027  imaidfu  50038  oppfvallem  50063  funcoppc3  50075  idfth  50086  idsubc  50088  uptposlem  50125  swapf2fn  50196  swapf1f1o  50203  swapf2f1o  50204  swapf2f1oaALT  50206  fucof1  50250  fucofn2  50252  fucofn22  50268  reldmprcof1  50309  reldmprcof2  50310  fucoppcid  50336  fucoppc  50338  functhinclem1  50372  fullthinc  50378  thincciso  50381  indcthing  50388  indthinc  50390  indthincALT  50391  functermc  50436  discsntermlem  50498  reldmlan2  50545  reldmran2  50546  rellan  50551  relran  50552  termolmd  50598  veronesev1lem  50808  veronesev2lem  50809  veronesev3lem  50810  veronesev4lem  50811  veronesev5lem  50812  veronesev6lem  50813  veronesevrowd  50814  veronesematrowd  50816