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  2393  nfald2  2444  nfabd2  2916  raleleq  3317  raleleqOLD  3318  ceqsexv2d  3502  dedhb  3677  csbie2df  4409  ssdifeq0  4453  r19.2zb  4462  dedth  4550  pwidg  4586  snidg  4627  rexreusng  4646  exsnrex  4647  ifpr  4660  rmosn  4686  rabrsn  4691  prid1g  4727  tpid1g  4736  tpid2g  4738  tpid3g  4739  pwpw0  4780  sssn  4793  elpreqpr  4834  unimax  4911  intmin3  4943  eqbrtrdi  5149  al0ssb  5266  rabelpw  5294  intabs  5307  difelpw  5312  0inp0  5317  axpr  5385  intidg  5420  copsexgw  5453  copsexg  5454  euotd  5476  elopab  5490  elvvuni  5718  posn  5727  frsn  5729  eqrelriv  5755  relsnb  5768  relopabiALT  5789  opabid2  5794  ididg  5820  iss  6009  dfpo2  6272  ord0eln0  6391  sucidg  6418  nsuceq0  6420  funopg  6553  fn0  6652  f00  6745  f0bi  6746  f10d  6837  f1o00  6838  fo00  6839  brprcneu  6851  brprcneuALT  6852  dffn5  6922  fsn  7110  funop  7124  funsndifnop  7126  fnsnbOLD  7143  eufnfv  7206  f1ounsn  7250  f1eqcocnv  7279  nfriotadw  7355  nfriotad  7358  riotaprop  7374  oprabidw  7421  oprabid  7422  elrnmpo  7528  ov6g  7556  ovelrn  7568  caovmo  7629  offn  7669  caofinvl  7688  fr3nr  7751  onprc  7757  ordeleqon  7761  onint0  7770  0elsuc  7813  onuninsuci  7819  orduninsuc  7822  ordzsl  7824  onzsl  7825  tfinds  7839  limomss  7850  limom  7861  peano5  7872  xpexr  7897  eqop2  8014  opreuopreu  8016  1stconst  8082  2ndconst  8083  frxp2  8126  frxp3  8133  funsssuppss  8172  dftpos3  8226  dftpos4  8227  oawordeulem  8521  omwordi  8538  nnmwordi  8602  riiner  8766  ecopover  8797  map0g  8860  mapsnd  8862  elixpsn  8913  en0  8992  en0ALT  8993  en0r  8994  en1  8998  snfi  9017  fiprc  9019  sbthlem2  9058  sbthlem4  9060  sbthlem5  9061  0domg  9074  findcard  9133  findcard2  9134  nneneq  9176  sdom1  9196  sdom1OLD  9197  1sdom2dom  9201  fineqvlem  9216  nfielex  9225  enp1i  9231  elfiun  9388  marypha1lem  9391  oicl  9489  oif  9490  oion  9496  hartogslem1  9502  hartogs  9504  wemapso2  9513  card2on  9514  0wdom  9530  brwdom2  9533  inf3lem6  9593  cantnflem3  9651  cantnflem4  9652  wemapwe  9657  cnfcom  9660  ssttrcl  9675  ttrclselem2  9686  tctr  9700  r1tr  9736  r1rankidb  9764  r1pw  9805  scottex  9845  scott0  9846  bnd2  9853  eldju2ndl  9884  tskwe  9910  oncard  9920  cardlim  9932  harsdom  9955  en2eleq  9968  dfac8alem  9989  cardaleph  10049  iunfictbso  10074  infmap2  10177  ackbij1lem18  10196  cff  10208  cfsuc  10217  cff1  10218  cflim2  10223  cfss  10225  sdom2en01  10262  infpssrlem4  10266  fin23lem7  10276  fin23lem11  10277  isfin2-2  10279  fin23lem26  10285  fin23lem19  10296  fin23lem17  10298  isf34lem2  10333  isf34lem4  10337  fin1a2lem6  10365  fin1a2lem10  10369  fin1a2lem12  10371  itunifn  10377  hsmexlem1  10386  axcc2lem  10396  dcomex  10407  axdc3lem4  10413  ondomon  10523  konigthlem  10528  pwcfsdom  10543  cfpwsdom  10544  axpowndlem3  10559  canth4  10607  canthnumlem  10608  canthwelem  10610  canthwe  10611  canthp1lem2  10613  pwfseqlem4  10622  pwfseqlem5  10623  gchaleph  10631  gch2  10635  winainflem  10653  0tsk  10715  rankcf  10737  tskcard  10741  gruina  10778  grutsk  10782  tskmid  10800  indpi  10867  nqereu  10889  mulcanenq  10920  recmulnq  10924  archnq  10940  ltsopr  10992  1ne0sr  11056  0idsr  11057  00sr  11059  leid  11277  lelttric  11288  divcan3  11870  divid  11875  div0  11877  lemul1a  12043  nn1suc  12215  nn0n0n1ge2b  12518  xnn0xr  12527  xnn0nemnf  12533  nn0lt10b  12603  nn0ind-raph  12641  elnn1uz2  12891  indstr2  12893  uzsupss  12906  rpnnen1lem4  12946  rpnnen1lem5  12947  xrnemnf  13084  xrnepnf  13085  mnfltxr  13094  xnn0n0n1ge2b  13099  xnn0ge0  13101  xrlttri  13106  xrlttr  13107  xrleid  13118  qbtwnxr  13167  xmullem2  13232  xlemul1a  13255  xrub  13279  reltxrnmnf  13310  ixxun  13329  xnn0xrge0  13474  fztpval  13554  fseq1p1m1  13566  elfznelfzob  13741  ltweuz  13933  fzfi  13944  fsuppmapnn0fiubex  13964  ser0f  14027  0exp  14069  faclbnd4lem1  14265  bcn1  14285  hashnemnf  14316  hashv01gt1  14317  hashsnle1  14389  hashgt12el2  14395  hashpw  14408  hashf1  14429  fz1isolem  14433  hash2prb  14444  hash3tpb  14467  0wrd0  14512  wrdlen1  14526  ccatvalfn  14553  eqs1  14584  wrdl1exs1  14585  swrdlen  14619  swrdwrdsymb  14634  swrdspsleq  14637  cats1un  14693  wrdind  14694  wrd2ind  14695  swrdccatin1  14697  repswsymballbi  14752  cshw1  14794  scshwfzeqfzo  14799  wrdl2exs2  14919  trclfvcotr  14982  relexp1g  14999  relexp0rel  15010  relexprelg  15011  relexpreld  15013  sqrt0  15214  sqrtsq  15242  mptfzshft  15751  prodf1f  15865  egt2lt3  16181  0dvds  16253  nn0onn  16357  nn0o  16360  divalgmod  16383  flodddiv4  16392  bitsp1o  16410  gcddvds  16480  bezout  16520  lcmdvds  16585  rpdvds  16637  1nprm  16656  prmind2  16662  dvdszzq  16698  nnoddn2prmb  16791  pcpre1  16820  vdwapf  16950  vdwapid1  16953  ram0  17000  ramz  17003  prmolefac  17024  cshws0  17079  prmlem0  17083  strle1  17135  restsspw  17401  prdsdsfn  17435  imasdsfn  17484  imasaddfnlem  17498  imasvscafn  17507  xpsfrnel  17532  isacs1i  17625  cidfn  17647  fnhomeqhomf  17659  comffn  17673  isoval  17734  sscres  17792  cofucl  17857  idffth  17904  ressffth  17909  cat1lem  18065  catcoppccl  18086  estrchomfn  18103  funcestrcsetclem4  18111  funcestrcsetclem7  18114  equivestrcsetc  18120  funcsetcestrclem4  18126  funcsetcestrclem7  18129  1stfcl  18165  2ndfcl  18166  prfcl  18171  evlfcl  18190  curf1cl  18196  curfcl  18200  hofcl  18227  yonedainv  18249  pospo  18311  lubfun  18318  glbfun  18331  joindmss  18345  meetdmss  18359  ipopos  18502  acsficl2d  18518  dirref  18567  mgmidcl  18600  mgmlrid  18601  ielefmnd  18821  smndex1basss  18839  smndex1n0mnd  18846  cntzssv  19267  idresperm  19323  symgvalstruct  19334  pmtrfmvdn0  19399  symggen  19407  psgnunilem1  19430  psgnprfval  19458  slwpgp  19550  frgpmhm  19702  frgpuptinv  19708  frgpup3lem  19714  gsumzoppg  19881  gsumcom2  19912  c0snmhm  20379  srhmsubc  20596  rhmsubclem1  20601  rrgsupp  20617  abv0  20739  zrhrhm  21428  psgnodpmr  21506  frlmphllem  21696  ellspd  21718  psrvscafval  21864  psrridm  21879  ltbwe  21958  psrbag0  21976  psrbagsn  21977  subrgascl  21980  psdmul  22060  mattpostpos  22348  mavmul0  22446  mavmul0g  22447  mdet0f1o  22487  m1detdiag  22491  m2detleiblem5  22519  m2detleiblem6  22520  m2detleiblem3  22523  m2detleiblem4  22524  maducoeval2  22534  d1mat2pmat  22633  chpmat1dlem  22729  chpmat1d  22730  baspartn  22848  eltg3  22856  topnex  22890  fctop  22898  cctop  22900  discld  22983  mretopd  22986  neipeltop  23023  neitr  23074  restcls  23075  ordtbaslem  23082  ordtuni  23084  idcn  23151  cnrmi  23254  cmpsublem  23293  cmpsub  23294  tgcmp  23295  uncmp  23297  hauscmplem  23300  cmpfi  23302  bwth  23304  1stcrestlem  23346  disllycmp  23392  dis1stc  23393  refref  23407  kgeni  23431  1stckgenlem  23447  kqffn  23619  snfil  23758  filconn  23777  cfinfil  23787  ufileu  23813  filufint  23814  fixufil  23816  cfinufil  23822  ufilen  23824  fin1aufil  23826  fmf  23839  rnelfm  23847  flimclslem  23878  hauspwpwf1  23881  supnfcls  23914  flimfnfcls  23922  fclscmp  23924  alexsubALTlem2  23942  alexsubALTlem3  23943  alexsubALT  23945  ptcmplem1  23946  cnextrel  23957  tsmsfbas  24022  ustref  24113  trust  24124  restutop  24132  isusp  24156  xmet0  24237  imasdsf1olem  24268  blfvalps  24278  blfps  24301  blf  24302  restmetu  24465  dscmet  24467  isngp2  24492  nm0  24524  nrginvrcn  24587  nmoix  24624  qdensere  24664  iccconn  24726  iccpnfcnv  24849  xrhmeo  24851  lebnumlem3  24869  metsscmetcld  25222  bcthlem5  25235  csschl  25283  rrxmfval  25313  minveclem3b  25335  cniccbdd  25369  ovolicc2lem4  25428  iunmbl  25461  ioorinv  25484  ioorcl  25485  i1f1lem  25597  limcvallem  25779  ellimc2  25785  limccnp  25799  limccnp2  25800  limcco  25801  perfdvf  25811  recnprss  25812  fncpn  25842  dvcmulf  25855  c1lip1  25909  lhop2  25927  q1pcl  26069  r1pdeglt  26072  ply1remlem  26077  plyssc  26112  ulm0  26307  cxpeq0  26594  cxplea  26612  cxplogb  26703  asinlem  26785  isppw2  27032  muval2  27051  dchrfi  27173  dchrpt  27185  bposlem6  27207  lgsdir2lem2  27244  lgsqr  27269  gausslemma2dlem4  27287  2lgslem2  27313  2lgslem3  27322  2lgs  27325  2sqlem7  27342  2sqlem11  27347  chtppilim  27393  nosgnn0i  27578  nolesgn2ores  27591  nogesgn1ores  27593  nosepnelem  27598  nosepdmlem  27602  nosupbnd1lem3  27629  nosupbnd1lem5  27631  nosupbnd2lem1  27634  noinfbnd1lem3  27644  noinfbnd1lem5  27646  noinfbnd2lem1  27649  oldval  27769  made0  27792  lrrecpo  27855  pncan2s  27985  divscan3d  28145  abssor  28155  om2noseqfo  28199  noseqrdglem  28206  noseqrdgfn  28207  noseqrdg0  28208  onsfi  28254  nohalf  28317  expsne0  28328  pw2divscan3d  28333  tgldimor  28436  tgcgr4  28465  tglnfn  28481  tglnunirn  28482  mirne  28601  mircinv  28602  perpln1  28644  perpln2  28645  lmiisolem  28730  xmstrkgc  28820  axcgrtr  28849  axsegconlem9  28859  axlowdimlem5  28880  axlowdimlem17  28892  axlowdim1  28893  uhgr0e  29005  edglnl  29077  uhgr0edgfi  29174  issubgr2  29206  subgrprop2  29208  egrsubgr  29211  0grsubgr  29212  0uhgrsubgr  29213  uhgrsubgrself  29214  nbgr1vtx  29292  nbgrssovtx  29295  nb3grprlem1  29314  uvtx01vtx  29331  cplgr1vlem  29363  cplgr1v  29364  usgrexilem  29374  wlkcomp  29566  wlk1walk  29574  wlkp1lem5  29612  uhgrwkspthlem1  29690  pthdlem1  29703  clwlkcomp  29716  lfgrn1cycl  29742  uspgrn2crct  29745  wwlksn0s  29798  umgrwwlks2on  29894  clwwlkn  29962  clwwlkn1  29977  0ewlk  30050  1ewlk  30051  0spth  30062  upgr1wlkdlem2  30082  wlk2v2e  30093  upgr3v3e3cycl  30116  upgr4cycl4dv4e  30121  eupth0  30150  frgr0v  30198  frgr1v  30207  1vwmgr  30212  ex-opab  30368  grpoinvf  30468  nvmid  30595  nmlnoubi  30732  hiidrcl  31031  hsn0elch  31184  shjshseli  31429  cmbr4i  31537  dfiop2  31689  kbpj  31892  nmopun  31950  adjeq0  32027  kbass2  32053  pjssdif1i  32111  pjinvari  32127  pjcmul2i  32138  pj3i  32144  stge1i  32174  stle0i  32175  sumdmdlem2  32355  dmdbr6ati  32359  dmdbr7ati  32360  rabsnel  32436  unidifsnel  32471  unidifsnne  32472  disjdifprg  32511  ofoprabco  32595  padct  32650  fpwrelmapffslem  32662  xrlelttric  32682  xnn0gt0  32699  iundisj2cnt  32729  f1ocnt  32732  fz1nnct  32733  fz1nntr  32734  hashxpe  32739  nn0min  32752  sgnmulsgn  32774  sgnmulsgp  32775  wrdt2ind  32882  xrge0tsmsbi  33010  opprabs  33460  rtelextdg2lem  33723  2sqr3minply  33777  locfinref  33838  dispcmp  33856  zartopn  33872  zarcmplem  33878  pstmxmet  33894  xrge0iifcnv  33930  xrge0iif1  33935  qqhre  34017  esumcl  34027  esumpr2  34064  esumpinfval  34070  esumpcvgval  34075  ofcfn  34097  pwsiga  34127  prsiga  34128  sigainb  34133  ldgenpisyslem1  34160  measiuns  34214  relfae  34244  pmeasmono  34322  sitgf  34345  eulerpartgbij  34370  signswch  34559  signslema  34560  signstlen  34565  signstfvn  34567  circlevma  34640  bnj216  34729  bnj151  34874  bnj517  34882  bnj970  34944  bnj1145  34990  bnj1498  35058  fineqvrep  35092  fineqvac  35094  wevgblacfn  35103  0nn0m1nnn0  35107  pthhashvtx  35122  acycgr0v  35142  prclisacycgr  35145  umgracycusgr  35148  cusgracyclt3v  35150  subfacp1lem5  35178  erdszelem8  35192  kur14lem1  35200  indispconn  35228  cvmsss2  35268  satfvsuclem2  35354  satfrel  35361  satfrnmapom  35364  satfv0fun  35365  satf00  35368  satf0suclem  35369  fmlasuc0  35378  msubrn  35523  dfon2lem7  35784  brbigcup  35893  elsingles  35913  fnimage  35924  funpartlem  35937  dfrdg4  35946  imagesset  35948  altopthsn  35956  elaltxp  35970  ellines  36147  linethru  36148  rankeq1o  36166  elhf2  36170  hfninf  36181  nn0prpwlem  36317  fneref  36345  neibastop2lem  36355  limsucncmpi  36440  bj-exlimmpbir  36909  curryset  36941  bj-snglex  36968  bj-restpw  37087  bj-inftyexpidisj  37205  topdifinffinlem  37342  relowlssretop  37358  rdgeqoa  37365  finxpreclem6  37391  fvineqsneq  37407  pibt2  37412  poimirlem23  37644  poimirlem29  37650  poimirlem31  37652  volsupnfl  37666  cnambfre  37669  dvasin  37705  dvacos  37706  sdclem2  37743  sstotbnd2  37775  ssbnd  37789  ismgmOLD  37851  grpokerinj  37894  rngomndo  37936  isdrngo1  37957  ac6s6  38173  iss2  38333  cnvelrels  38493  cosselrels  38494  brssrid  38500  brcnvssrid  38505  dfdisjs5  38711  eldisjs5  38725  mpets2  38840  pets  38851  prtlem12  38867  riotasv2d  38957  lkrscss  39098  islshpkrN  39120  isline  39740  ispointN  39743  0psubN  39750  linepsubN  39753  atpsubN  39754  cdlemk36  40914  diafn  41035  dibfna  41155  dibvalrel  41164  dicvalrelN  41186  diclspsn  41195  dihvalrel  41280  dih1  41287  lclkrlem1  41507  lclkr  41534  mapd1o  41649  mapdin  41663  hdmapfnN  41830  hgmapfnN  41889  lcmineqlem10  42033  sticksstones9  42149  sn-iotalem  42216  readvrec2  42356  readvrec  42357  repncan2  42377  elrfirn  42690  ismrcd1  42693  istopclsd  42695  rabren3dioph  42810  jm2.17b  42957  jm2.22  42991  jm2.23  42992  ttac  43032  pw2f1ocnv  43033  dnnumch1  43040  hbtlem5  43124  mncn0  43135  aaitgo  43158  rngunsnply  43165  unielss  43214  onexlimgt  43239  cantnfresb  43320  dflim5  43325  naddwordnexlem4  43397  safesnsupfiss  43411  safesnsupfidom1o  43413  safesnsupfilb  43414  ensucne0OLD  43526  clcnvlem  43619  relexp01min  43709  ntrf  44119  ssrecnpr  44304  seff  44305  sblpnf  44306  nzss  44313  dvconstbi  44330  ipo0  44445  ifr0  44446  addrfn  44468  subrfn  44469  mulvfn  44470  wfaxrep  44991  refsum2cnlem1  45038  rn1st  45274  ellimciota  45619  dvmptconst  45920  dvmptidg  45922  dvmulcncf  45930  dvdivcncf  45932  stoweidlem26  46031  stoweidlem50  46055  stoweidlem57  46062  aiotaval  47100  ndfatafv2nrn  47226  afv2ndefb  47229  funop1  47288  fun2dmnopgexmpl  47289  2ffzoeq  47332  2ltceilhalf  47333  m1modne  47353  iccpartiltu  47427  iccpartigtl  47428  zofldiv2ALTV  47667  evenprm2  47719  9fppr8  47742  stgoldbwt  47781  nnsum3primesle9  47799  nnsum4primeseven  47805  nnsum4primesevenALTV  47806  tgblthelfgott  47820  dfclnbgr6  47860  cycl3grtri  47950  grtrimap  47951  stgredgel  47960  stgr1  47964  isubgr3stgrlem2  47970  isubgr3stgrlem3  47971  usgrexmpl2trifr  48032  gpg5nbgrvtx13starlem1  48066  gpg5nbgrvtx13starlem2  48067  gpg5nbgrvtx13starlem3  48068  gpg5nbgr3star  48076  gpg3kgrtriex  48084  uspgrex  48142  0mgm  48158  nnsgrpmgm  48168  rngchomffvalALTV  48270  rhmsubcALTVlem1  48273  funcringcsetcALTV2lem4  48285  funcringcsetclem4ALTV  48308  srhmsubcALTV  48317  mapsnop  48336  zlmodzxzldeplem4  48496  zofldiv2  48524  fdivval  48532  nnlog2ge0lt1  48559  dig1  48601  itcoval2  48657  itcoval3  48658  mosn  48805  mo0  48806  mof02  48831  mofeu  48840  f102g  48844  f1mo  48845  tposres0  48869  f1omo  48885  f1omoOLD  48886  resipos  48967  intubeu  48976  unilbeu  48977  sectfn  49022  nelsubclem  49060  idfu1stf1o  49092  imaidfu  49103  oppfvallem  49128  funcoppc3  49140  idfth  49151  idsubc  49153  uptposlem  49190  swapf2fn  49261  swapf1f1o  49268  swapf2f1o  49269  swapf2f1oaALT  49271  fucof1  49315  fucofn2  49317  fucofn22  49333  reldmprcof1  49374  reldmprcof2  49375  fucoppcid  49401  fucoppc  49403  functhinclem1  49437  fullthinc  49443  thincciso  49446  indcthing  49453  indthinc  49455  indthincALT  49456  functermc  49501  discsntermlem  49563  reldmlan2  49610  reldmran2  49611  rellan  49616  relran  49617  termolmd  49663