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  1083  spei  2399  nfald2  2450  nfabd2  2923  raleleq  3313  raleleqOLD  3314  ceqsexv2d  3492  dedhb  3662  csbie2df  4396  ssdifeq0  4440  dedth  4539  pwidg  4575  snidg  4618  rexreusng  4637  exsnrex  4638  ifpr  4651  rmosn  4677  rabrsn  4682  prid1g  4718  tpid1g  4727  tpid2g  4729  tpid3g  4730  pwpw0  4770  sssn  4783  elpreqpr  4824  unimax  4901  intmin3  4932  eqbrtrdi  5138  al0ssb  5254  rabelpw  5282  intabs  5295  difelpw  5300  0inp0  5305  axpr  5373  intidg  5406  copsexgw  5439  copsexg  5440  euotd  5462  elopab  5476  elvvuni  5702  posn  5711  frsn  5713  eqrelriv  5739  relsnb  5752  relopabiALT  5773  opabid2  5778  ididg  5803  iss  5995  dfpo2  6255  ord0eln0  6374  sucidg  6401  nsuceq0  6403  funopg  6527  fn0  6624  f00  6717  f0bi  6718  f10d  6809  f1o00  6810  fo00  6811  brprcneu  6825  brprcneuALT  6826  dffn5  6893  fsn  7083  funop  7097  funsndifnop  7099  fnsnbOLD  7115  eufnfv  7178  f1ounsn  7221  f1eqcocnv  7250  nfriotadw  7326  nfriotad  7329  riotaprop  7345  oprabidw  7392  oprabid  7393  elrnmpo  7497  ov6g  7525  ovelrn  7537  caovmo  7598  offn  7638  caofinvl  7657  fr3nr  7720  onprc  7726  ordeleqon  7730  onint0  7739  0elsuc  7780  onuninsuci  7785  orduninsuc  7788  ordzsl  7790  onzsl  7791  tfinds  7805  limomss  7816  limom  7827  peano5  7838  xpexr  7863  eqop2  7979  opreuopreu  7981  1stconst  8045  2ndconst  8046  frxp2  8089  frxp3  8096  funsssuppss  8135  dftpos3  8189  dftpos4  8190  oawordeulem  8484  omwordi  8501  nnmwordi  8566  riiner  8732  ecopover  8763  map0g  8827  mapsnd  8829  elixpsn  8880  en0  8960  en0ALT  8961  en0r  8962  en1  8966  snfi  8985  fiprc  8986  sbthlem2  9021  sbthlem4  9023  sbthlem5  9024  0domg  9037  findcard  9093  findcard2  9094  nneneq  9135  sdom1  9155  1sdom2dom  9159  fineqvlem  9171  nfielex  9179  enp1i  9184  elfiun  9338  marypha1lem  9341  oicl  9439  oif  9440  oion  9446  hartogslem1  9452  hartogs  9454  wemapso2  9463  card2on  9464  0wdom  9480  brwdom2  9483  inf3lem6  9547  cantnflem3  9605  cantnflem4  9606  wemapwe  9611  cnfcom  9614  ssttrcl  9629  ttrclselem2  9640  tctr  9652  r1tr  9693  r1rankidb  9721  r1pw  9762  scottex  9802  scott0  9803  bnd2  9810  eldju2ndl  9841  tskwe  9867  oncard  9877  cardlim  9889  harsdom  9912  en2eleq  9923  dfac8alem  9944  cardaleph  10004  iunfictbso  10029  infmap2  10132  ackbij1lem18  10151  cff  10163  cfsuc  10172  cff1  10173  cflim2  10178  cfss  10180  sdom2en01  10217  infpssrlem4  10221  fin23lem7  10231  fin23lem11  10232  isfin2-2  10234  fin23lem26  10240  fin23lem19  10251  fin23lem17  10253  isf34lem2  10288  isf34lem4  10292  fin1a2lem6  10320  fin1a2lem10  10324  fin1a2lem12  10326  itunifn  10332  hsmexlem1  10341  axcc2lem  10351  dcomex  10362  axdc3lem4  10368  ondomon  10478  konigthlem  10484  pwcfsdom  10499  cfpwsdom  10500  axpowndlem3  10515  canth4  10563  canthnumlem  10564  canthwelem  10566  canthwe  10567  canthp1lem2  10569  pwfseqlem4  10578  pwfseqlem5  10579  gchaleph  10587  gch2  10591  winainflem  10609  0tsk  10671  rankcf  10693  tskcard  10697  gruina  10734  grutsk  10738  tskmid  10756  indpi  10823  nqereu  10845  mulcanenq  10876  recmulnq  10880  archnq  10896  ltsopr  10948  1ne0sr  11012  0idsr  11013  00sr  11015  leid  11234  lelttric  11245  divcan3  11827  divid  11832  div0  11834  lemul1a  12000  nn1suc  12172  nn0n0n1ge2b  12475  xnn0xr  12484  xnn0nemnf  12490  nn0lt10b  12559  nn0ind-raph  12597  elnn1uz2  12843  indstr2  12845  uzsupss  12858  rpnnen1lem4  12898  rpnnen1lem5  12899  xrnemnf  13036  xrnepnf  13037  mnfltxr  13046  xnn0n0n1ge2b  13051  xnn0ge0  13053  xrlttri  13058  xrlttr  13059  xrleid  13070  qbtwnxr  13120  xmullem2  13185  xlemul1a  13208  xrub  13232  reltxrnmnf  13263  ixxun  13282  xnn0xrge0  13427  fztpval  13507  fseq1p1m1  13519  elfznelfzob  13695  ltweuz  13889  fzfi  13900  fsuppmapnn0fiubex  13920  ser0f  13983  0exp  14025  faclbnd4lem1  14221  bcn1  14241  hashnemnf  14272  hashv01gt1  14273  hashsnle1  14345  hashgt12el2  14351  hashpw  14364  hashf1  14385  fz1isolem  14389  hash2prb  14400  hash3tpb  14423  0wrd0  14468  wrdlen1  14482  ccatvalfn  14509  eqs1  14541  wrdl1exs1  14542  swrdlen  14576  swrdwrdsymb  14591  swrdspsleq  14594  cats1un  14649  wrdind  14650  wrd2ind  14651  swrdccatin1  14653  repswsymballbi  14708  cshw1  14750  scshwfzeqfzo  14754  wrdl2exs2  14874  trclfvcotr  14937  relexp1g  14954  relexp0rel  14965  relexprelg  14966  relexpreld  14968  sqrt0  15169  sqrtsq  15197  mptfzshft  15706  prodf1f  15820  egt2lt3  16136  0dvds  16208  nn0onn  16312  nn0o  16315  divalgmod  16338  flodddiv4  16347  bitsp1o  16365  gcddvds  16435  bezout  16475  lcmdvds  16540  rpdvds  16592  1nprm  16611  prmind2  16617  dvdszzq  16653  nnoddn2prmb  16746  pcpre1  16775  vdwapf  16905  vdwapid1  16908  ram0  16955  ramz  16958  prmolefac  16979  cshws0  17034  prmlem0  17038  strle1  17090  restsspw  17356  prdsdsfn  17390  imasdsfn  17440  imasaddfnlem  17454  imasvscafn  17463  xpsfrnel  17488  isacs1i  17585  cidfn  17607  fnhomeqhomf  17619  comffn  17633  isoval  17694  sscres  17752  cofucl  17817  idffth  17864  ressffth  17869  cat1lem  18025  catcoppccl  18046  estrchomfn  18063  funcestrcsetclem4  18071  funcestrcsetclem7  18074  equivestrcsetc  18080  funcsetcestrclem4  18086  funcsetcestrclem7  18089  1stfcl  18125  2ndfcl  18126  prfcl  18131  evlfcl  18150  curf1cl  18156  curfcl  18160  hofcl  18187  yonedainv  18209  pospo  18271  lubfun  18278  glbfun  18291  joindmss  18305  meetdmss  18319  ipopos  18464  acsficl2d  18480  dirref  18529  mgmidcl  18596  mgmlrid  18597  ielefmnd  18817  smndex1basss  18835  smndex1n0mnd  18842  cntzssv  19262  idresperm  19320  symgvalstruct  19331  pmtrfmvdn0  19396  symggen  19404  psgnunilem1  19427  psgnprfval  19455  slwpgp  19547  frgpmhm  19699  frgpuptinv  19705  frgpup3lem  19711  gsumzoppg  19878  gsumcom2  19909  c0snmhm  20404  srhmsubc  20618  rhmsubclem1  20623  rrgsupp  20639  abv0  20761  zrhrhm  21471  psgnodpmr  21550  frlmphllem  21740  ellspd  21762  psrvscafval  21909  psrridm  21923  ltbwe  22004  psrbag0  22022  psrbagsn  22023  subrgascl  22026  psdmul  22114  mattpostpos  22403  mavmul0  22501  mavmul0g  22502  mdet0f1o  22542  m1detdiag  22546  m2detleiblem5  22574  m2detleiblem6  22575  m2detleiblem3  22578  m2detleiblem4  22579  maducoeval2  22589  d1mat2pmat  22688  chpmat1dlem  22784  chpmat1d  22785  baspartn  22903  eltg3  22911  topnex  22945  fctop  22953  cctop  22955  discld  23038  mretopd  23041  neipeltop  23078  neitr  23129  restcls  23130  ordtbaslem  23137  ordtuni  23139  idcn  23206  cnrmi  23309  cmpsublem  23348  cmpsub  23349  tgcmp  23350  uncmp  23352  hauscmplem  23355  cmpfi  23357  bwth  23359  1stcrestlem  23401  disllycmp  23447  dis1stc  23448  refref  23462  kgeni  23486  1stckgenlem  23502  kqffn  23674  snfil  23813  filconn  23832  cfinfil  23842  ufileu  23868  filufint  23869  fixufil  23871  cfinufil  23877  ufilen  23879  fin1aufil  23881  fmf  23894  rnelfm  23902  flimclslem  23933  hauspwpwf1  23936  supnfcls  23969  flimfnfcls  23977  fclscmp  23979  alexsubALTlem2  23997  alexsubALTlem3  23998  alexsubALT  24000  ptcmplem1  24001  cnextrel  24012  tsmsfbas  24077  ustref  24168  trust  24178  restutop  24186  isusp  24210  xmet0  24291  imasdsf1olem  24322  blfvalps  24332  blfps  24355  blf  24356  restmetu  24519  dscmet  24521  isngp2  24546  nm0  24578  nrginvrcn  24641  nmoix  24678  qdensere  24718  iccconn  24780  iccpnfcnv  24903  xrhmeo  24905  lebnumlem3  24923  metsscmetcld  25276  bcthlem5  25289  csschl  25337  rrxmfval  25367  minveclem3b  25389  cniccbdd  25423  ovolicc2lem4  25482  iunmbl  25515  ioorinv  25538  ioorcl  25539  i1f1lem  25651  limcvallem  25833  ellimc2  25839  limccnp  25853  limccnp2  25854  limcco  25855  perfdvf  25865  recnprss  25866  fncpn  25896  dvcmulf  25909  c1lip1  25963  lhop2  25981  q1pcl  26123  r1pdeglt  26126  ply1remlem  26131  plyssc  26166  ulm0  26361  cxpeq0  26648  cxplea  26666  cxplogb  26757  asinlem  26839  isppw2  27086  muval2  27105  dchrfi  27227  dchrpt  27239  bposlem6  27261  lgsdir2lem2  27298  lgsqr  27323  gausslemma2dlem4  27341  2lgslem2  27367  2lgslem3  27376  2lgs  27379  2sqlem7  27396  2sqlem11  27401  chtppilim  27447  nosgnn0i  27632  nolesgn2ores  27645  nogesgn1ores  27647  nosepnelem  27652  nosepdmlem  27656  nosupbnd1lem3  27683  nosupbnd1lem5  27685  nosupbnd2lem1  27688  noinfbnd1lem3  27698  noinfbnd1lem5  27700  noinfbnd2lem1  27703  oldval  27835  made0  27864  lrrecpo  27942  pncan2s  28075  divscan3d  28237  abssor  28247  om2noseqfo  28299  noseqrdglem  28306  noseqrdgfn  28307  noseqrdg0  28308  onsfi  28357  nohalf  28425  expsne0  28437  pw2divscan3d  28442  tgldimor  28579  tgcgr4  28608  tglnfn  28624  tglnunirn  28625  mirne  28744  mircinv  28745  perpln1  28787  perpln2  28788  lmiisolem  28873  xmstrkgc  28963  axcgrtr  28993  axsegconlem9  29003  axlowdimlem5  29024  axlowdimlem17  29036  axlowdim1  29037  uhgr0e  29149  edglnl  29221  uhgr0edgfi  29318  issubgr2  29350  subgrprop2  29352  egrsubgr  29355  0grsubgr  29356  0uhgrsubgr  29357  uhgrsubgrself  29358  nbgr1vtx  29436  nbgrssovtx  29439  nb3grprlem1  29458  uvtx01vtx  29475  cplgr1vlem  29507  cplgr1v  29508  usgrexilem  29518  wlkcomp  29709  wlk1walk  29717  wlkp1lem5  29754  uhgrwkspthlem1  29831  pthdlem1  29844  clwlkcomp  29857  lfgrn1cycl  29883  uspgrn2crct  29886  wwlksn0s  29939  usgrwwlks2on  30036  umgrwwlks2on  30037  clwwlkn  30106  clwwlkn1  30121  0ewlk  30194  1ewlk  30195  0spth  30206  upgr1wlkdlem2  30226  wlk2v2e  30237  upgr3v3e3cycl  30260  upgr4cycl4dv4e  30265  eupth0  30294  frgr0v  30342  frgr1v  30351  1vwmgr  30356  ex-opab  30512  grpoinvf  30612  nvmid  30739  nmlnoubi  30876  hiidrcl  31175  hsn0elch  31328  shjshseli  31573  cmbr4i  31681  dfiop2  31833  kbpj  32036  nmopun  32094  adjeq0  32171  kbass2  32197  pjssdif1i  32255  pjinvari  32271  pjcmul2i  32282  pj3i  32288  stge1i  32318  stle0i  32319  sumdmdlem2  32499  dmdbr6ati  32503  dmdbr7ati  32504  rabsnel  32579  unidifsnel  32614  unidifsnne  32615  disjdifprg  32654  ofoprabco  32746  padct  32800  fpwrelmapffslem  32814  nn0mnfxrd  32834  xrlelttric  32835  xnn0gt0  32852  iundisj2cnt  32882  f1ocnt  32883  fz1nnct  32884  fz1nntr  32885  hashxpe  32890  nn0min  32904  sgnmulsgn  32926  sgnmulsgp  32927  wrdt2ind  33038  xrge0tsmsbi  33160  opprabs  33567  rtelextdg2lem  33896  2sqr3minply  33950  locfinref  34011  dispcmp  34029  zartopn  34045  zarcmplem  34051  pstmxmet  34067  xrge0iifcnv  34103  xrge0iif1  34108  qqhre  34190  esumcl  34200  esumpr2  34237  esumpinfval  34243  esumpcvgval  34248  ofcfn  34270  pwsiga  34300  prsiga  34301  sigainb  34306  ldgenpisyslem1  34333  measiuns  34387  relfae  34417  pmeasmono  34494  sitgf  34517  eulerpartgbij  34542  signswch  34731  signslema  34732  signstlen  34737  signstfvn  34739  circlevma  34812  bnj216  34901  bnj151  35046  bnj517  35054  bnj970  35116  bnj1145  35162  bnj1498  35230  r1omhfb  35281  fineqvrep  35283  fineqvac  35285  fineqvnttrclselem1  35290  fineqvnttrclselem2  35291  fineqvnttrclse  35293  fineqvinfep  35294  r1omhfbregs  35306  wevgblacfn  35316  0nn0m1nnn0  35320  pthhashvtx  35335  acycgr0v  35355  prclisacycgr  35358  umgracycusgr  35361  cusgracyclt3v  35363  subfacp1lem5  35391  erdszelem8  35405  kur14lem1  35413  indispconn  35441  cvmsss2  35481  satfvsuclem2  35567  satfrel  35574  satfrnmapom  35577  satfv0fun  35578  satf00  35581  satf0suclem  35582  fmlasuc0  35591  msubrn  35736  dfon2lem7  35994  brbigcup  36103  elsingles  36123  fnimage  36134  funpartlem  36149  dfrdg4  36158  imagesset  36160  altopthsn  36168  elaltxp  36182  ellines  36359  linethru  36360  rankeq1o  36378  elhf2  36382  hfninf  36393  nn0prpwlem  36529  fneref  36557  neibastop2lem  36567  limsucncmpi  36652  bj-exlimmpbir  37128  curryset  37160  bj-snglex  37187  bj-restpw  37310  bj-inftyexpidisj  37428  topdifinffinlem  37565  relowlssretop  37581  rdgeqoa  37588  finxpreclem6  37614  fvineqsneq  37630  pibt2  37635  poimirlem23  37857  poimirlem29  37863  poimirlem31  37865  volsupnfl  37879  cnambfre  37882  dvasin  37918  dvacos  37919  sdclem2  37956  sstotbnd2  37988  ssbnd  38002  ismgmOLD  38064  grpokerinj  38107  rngomndo  38149  isdrngo1  38170  ac6s6  38386  iss2  38558  relecxrn  38621  sucmapsuc  38703  cosselrels  38789  cnvelrels  38790  brssrid  38796  brcnvssrid  38801  dfdisjs5  39011  eldisjs5  39037  eldisjsim3  39151  mpets2  39169  pets  39180  prtlem12  39206  riotasv2d  39296  lkrscss  39437  islshpkrN  39459  isline  40078  ispointN  40081  0psubN  40088  linepsubN  40091  atpsubN  40092  cdlemk36  41252  diafn  41373  dibfna  41493  dibvalrel  41502  dicvalrelN  41524  diclspsn  41533  dihvalrel  41618  dih1  41625  lclkrlem1  41845  lclkr  41872  mapd1o  41987  mapdin  42001  hdmapfnN  42168  hgmapfnN  42227  lcmineqlem10  42371  sticksstones9  42487  sn-iotalem  42556  readvrec2  42694  readvrec  42695  repncan2  42715  elrfirn  43015  ismrcd1  43018  istopclsd  43020  rabren3dioph  43135  jm2.17b  43281  jm2.22  43315  jm2.23  43316  ttac  43356  pw2f1ocnv  43357  dnnumch1  43364  hbtlem5  43448  mncn0  43459  aaitgo  43482  rngunsnply  43489  unielss  43538  onexlimgt  43563  cantnfresb  43644  dflim5  43649  naddwordnexlem4  43721  safesnsupfiss  43734  safesnsupfidom1o  43736  safesnsupfilb  43737  ensucne0OLD  43849  clcnvlem  43942  relexp01min  44032  ntrf  44442  ssrecnpr  44627  seff  44628  sblpnf  44629  nzss  44636  dvconstbi  44653  ipo0  44767  ifr0  44768  addrfn  44790  subrfn  44791  mulvfn  44792  wfaxrep  45313  refsum2cnlem1  45360  rn1st  45594  ellimciota  45937  dvmptconst  46236  dvmptidg  46238  dvmulcncf  46246  dvdivcncf  46248  stoweidlem26  46347  stoweidlem50  46371  stoweidlem57  46378  aiotaval  47418  ndfatafv2nrn  47544  afv2ndefb  47547  funop1  47606  fun2dmnopgexmpl  47607  2ffzoeq  47650  2ltceilhalf  47651  m1modne  47671  iccpartiltu  47745  iccpartigtl  47746  zofldiv2ALTV  47985  evenprm2  48037  9fppr8  48060  stgoldbwt  48099  nnsum3primesle9  48117  nnsum4primeseven  48123  nnsum4primesevenALTV  48124  tgblthelfgott  48138  dfclnbgr6  48179  cycl3grtri  48270  grtrimap  48271  stgredgel  48280  stgr1  48284  isubgr3stgrlem2  48290  isubgr3stgrlem3  48291  usgrexmpl2trifr  48360  gpg5nbgrvtx13starlem1  48394  gpg5nbgrvtx13starlem2  48395  gpg5nbgrvtx13starlem3  48396  gpg5nbgr3star  48404  gpg3kgrtriex  48412  uspgrex  48473  0mgm  48489  nnsgrpmgm  48499  rngchomffvalALTV  48601  rhmsubcALTVlem1  48604  funcringcsetcALTV2lem4  48616  funcringcsetclem4ALTV  48639  srhmsubcALTV  48648  mapsnop  48667  zlmodzxzldeplem4  48826  zofldiv2  48854  fdivval  48862  nnlog2ge0lt1  48889  dig1  48931  itcoval2  48987  itcoval3  48988  mosn  49135  mo0  49136  mof02  49161  mofeu  49170  f102g  49174  f1mo  49175  tposres0  49199  f1omo  49215  f1omoOLD  49216  resipos  49297  intubeu  49306  unilbeu  49307  sectfn  49351  nelsubclem  49389  idfu1stf1o  49421  imaidfu  49432  oppfvallem  49457  funcoppc3  49469  idfth  49480  idsubc  49482  uptposlem  49519  swapf2fn  49590  swapf1f1o  49597  swapf2f1o  49598  swapf2f1oaALT  49600  fucof1  49644  fucofn2  49646  fucofn22  49662  reldmprcof1  49703  reldmprcof2  49704  fucoppcid  49730  fucoppc  49732  functhinclem1  49766  fullthinc  49772  thincciso  49775  indcthing  49782  indthinc  49784  indthincALT  49785  functermc  49830  discsntermlem  49892  reldmlan2  49939  reldmran2  49940  rellan  49945  relran  49946  termolmd  49992