Theorem mpbiri 257

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

Syntax hints:   → wi 4   ↔ wb 205

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 206

This theorem is referenced by:  elimh  1083  spei  2392  nfald2  2443  nfabd2  2928  raleleqALT  3316  dedhb  3664  sbceqalOLD  3809  csbie2df  4405  ssdifeq0  4449  r19.2zb  4458  dedth  4549  pwidg  4585  elpr2OLD  4617  snidg  4625  rexreusng  4645  exsnrex  4646  ifpr  4657  rmosn  4685  rabrsn  4690  prid1g  4726  tpid1g  4735  tpid2g  4737  tpid3g  4738  pwpw0  4778  sssn  4791  elpreqpr  4829  pwsnOLD  4863  unimax  4910  intmin3  4942  eqbrtrdi  5149  al0ssb  5270  intabs  5304  pwnss  5311  difelpw  5313  rabelpw  5314  0inp0  5319  intidg  5419  copsexgw  5452  copsexg  5453  euotd  5475  elopab  5489  elvvuni  5713  posn  5722  frsn  5724  eqrelriv  5750  relsnb  5763  relopabiALT  5784  opabid2  5789  ididg  5814  iss  5994  dfpo2  6253  ord0eln0  6377  sucidg  6403  nsuceq0  6405  funopg  6540  fn0  6637  f00  6729  f0bi  6730  f10d  6823  f1o00  6824  fo00  6825  brprcneu  6837  brprcneuALT  6838  dffn5  6906  fsn  7086  funop  7100  funsndifnop  7102  fnsnb  7117  eufnfv  7184  f1eqcocnv  7252  f1eqcocnvOLD  7253  nfriotadw  7326  nfriotad  7330  riotaprop  7346  oprabidw  7393  oprabid  7394  elrnmpo  7497  ov6g  7523  ovelrn  7535  caovmo  7596  offn  7635  caofinvl  7652  fr3nr  7711  onprc  7717  ordeleqon  7721  onint0  7731  0elsuc  7775  onuninsuci  7781  orduninsuc  7784  ordzsl  7786  onzsl  7787  tfinds  7801  limomss  7812  limom  7823  peano5  7835  peano5OLD  7836  xpexr  7860  eqop2  7969  opreuopreu  7971  1stconst  8037  2ndconst  8038  frxp2  8081  frxp3  8088  funsssuppss  8126  dftpos3  8180  dftpos4  8181  wfrlem4OLD  8263  wfrlem14OLD  8273  oawordeulem  8506  omwordi  8523  nnmwordi  8587  riiner  8736  ecopover  8767  map0g  8829  mapsnd  8831  elixpsn  8882  en0  8964  en0OLD  8965  en0ALT  8966  en0r  8967  en1  8972  en1OLD  8973  fiprc  8996  sbthlem2  9035  sbthlem4  9037  sbthlem5  9038  0domg  9051  findcard  9114  findcard2  9115  nneneq  9160  nneneqOLD  9172  sdom1  9193  sdom1OLD  9194  1sdom2dom  9198  fineqvlem  9213  nfielex  9224  enp1i  9230  findcard2OLD  9235  elfiun  9375  marypha1lem  9378  oicl  9474  oif  9475  oion  9481  hartogslem1  9487  hartogs  9489  wemapso2  9498  card2on  9499  0wdom  9515  brwdom2  9518  inf3lem6  9578  cantnflem3  9636  cantnflem4  9637  wemapwe  9642  cnfcom  9645  ssttrcl  9660  ttrclselem2  9671  tctr  9685  r1tr  9721  r1rankidb  9749  r1pw  9790  scottex  9830  scott0  9831  bnd2  9838  eldju2ndl  9869  tskwe  9895  oncard  9905  cardlim  9917  harsdom  9940  en2eleq  9953  dfac8alem  9974  cardaleph  10034  iunfictbso  10059  infmap2  10163  ackbij1lem18  10182  cff  10193  cfsuc  10202  cff1  10203  cflim2  10208  cfss  10210  sdom2en01  10247  infpssrlem4  10251  fin23lem7  10261  fin23lem11  10262  isfin2-2  10264  fin23lem26  10270  fin23lem19  10281  fin23lem17  10283  isf34lem2  10318  isf34lem4  10322  fin1a2lem6  10350  fin1a2lem10  10354  fin1a2lem12  10356  itunifn  10362  hsmexlem1  10371  axcc2lem  10381  dcomex  10392  axdc3lem4  10398  ondomon  10508  konigthlem  10513  pwcfsdom  10528  cfpwsdom  10529  axpowndlem3  10544  canth4  10592  canthnumlem  10593  canthwelem  10595  canthwe  10596  canthp1lem2  10598  pwfseqlem4  10607  pwfseqlem5  10608  gchaleph  10616  gch2  10620  winainflem  10638  0tsk  10700  rankcf  10722  tskcard  10726  gruina  10763  grutsk  10767  tskmid  10785  indpi  10852  nqereu  10874  mulcanenq  10905  recmulnq  10909  archnq  10925  ltsopr  10977  1ne0sr  11041  0idsr  11042  00sr  11044  leid  11260  lelttric  11271  divcan3  11848  lemul1a  12018  nn1suc  12184  nn0n0n1ge2b  12490  xnn0xr  12499  xnn0nemnf  12505  nn0lt10b  12574  nn0ind-raph  12612  elnn1uz2  12859  indstr2  12861  uzsupss  12874  rpnnen1lem4  12914  rpnnen1lem5  12915  xrnemnf  13047  xrnepnf  13048  mnfltxr  13057  xnn0n0n1ge2b  13061  xnn0ge0  13063  xrlttri  13068  xrlttr  13069  xrleid  13080  qbtwnxr  13129  xmullem2  13194  xlemul1a  13217  xrub  13241  reltxrnmnf  13271  ixxun  13290  xnn0xrge0  13433  fztpval  13513  fseq1p1m1  13525  elfznelfzob  13688  ltweuz  13876  fzfi  13887  fsuppmapnn0fiubex  13907  ser0f  13971  0exp  14013  faclbnd4lem1  14203  bcn1  14223  hashnemnf  14254  hashv01gt1  14255  hashsnle1  14327  hashgt12el2  14333  hashpw  14346  hashf1  14368  fz1isolem  14372  hash2prb  14383  0wrd0  14440  wrdlen1  14454  ccatvalfn  14481  eqs1  14512  wrdl1exs1  14513  swrdlen  14547  swrdwrdsymb  14562  swrdspsleq  14565  cats1un  14621  wrdind  14622  wrd2ind  14623  swrdccatin1  14625  repswsymballbi  14680  cshw1  14722  scshwfzeqfzo  14727  wrdl2exs2  14847  trclfvcotr  14906  relexp1g  14923  relexp0rel  14934  relexprelg  14935  relexpreld  14937  sqrt0  15138  sqrtsq  15166  mptfzshft  15674  prodf1f  15788  egt2lt3  16099  0dvds  16170  nn0onn  16273  nn0o  16276  divalgmod  16299  flodddiv4  16306  bitsp1o  16324  gcddvds  16394  bezout  16435  lcmdvds  16495  rpdvds  16547  1nprm  16566  prmind2  16572  nnoddn2prmb  16696  pcpre1  16725  vdwapf  16855  vdwapid1  16858  ram0  16905  ramz  16908  prmolefac  16929  cshws0  16985  prmlem0  16989  strle1  17041  restsspw  17327  prdsdsfn  17361  imasdsfn  17410  imasaddfnlem  17424  imasvscafn  17433  xpsfrnel  17458  isacs1i  17551  cidfn  17573  fnhomeqhomf  17585  comffn  17599  isoval  17662  sscres  17720  cofucl  17788  idffth  17834  ressffth  17839  cat1lem  17996  catcoppccl  18017  catcoppcclOLD  18018  estrchomfn  18036  funcestrcsetclem4  18045  funcestrcsetclem7  18048  equivestrcsetc  18054  funcsetcestrclem4  18060  funcsetcestrclem7  18063  1stfcl  18099  2ndfcl  18100  prfcl  18105  evlfcl  18125  curf1cl  18131  curfcl  18135  hofcl  18162  yonedainv  18184  pospo  18248  lubfun  18255  glbfun  18268  joindmss  18282  meetdmss  18296  ipopos  18439  acsficl2d  18455  dirref  18504  mgmidcl  18535  mgmlrid  18536  ielefmnd  18711  smndex1basss  18729  smndex1n0mnd  18736  cntzssv  19122  idresperm  19181  symgvalstruct  19192  symgvalstructOLD  19193  pmtrfmvdn0  19258  symggen  19266  psgnunilem1  19289  psgnprfval  19317  slwpgp  19409  frgpmhm  19561  frgpuptinv  19567  frgpup3lem  19573  gsumzoppg  19735  gsumcom2  19766  abv0  20346  rrgsupp  20798  zrhrhm  20949  psgnodpmr  21031  frlmphllem  21223  frlmphl  21224  ellspd  21245  psrvscafval  21395  psrridm  21410  ltbwe  21482  psrbag0  21507  psrbagsn  21508  subrgascl  21511  mattpostpos  21840  mavmul0  21938  mavmul0g  21939  mdet0f1o  21979  m1detdiag  21983  m2detleiblem5  22011  m2detleiblem6  22012  m2detleiblem3  22015  m2detleiblem4  22016  maducoeval2  22026  d1mat2pmat  22125  chpmat1dlem  22221  chpmat1d  22222  baspartn  22341  eltg3  22349  topnex  22383  fctop  22391  cctop  22393  discld  22477  mretopd  22480  neipeltop  22517  neitr  22568  restcls  22569  ordtbaslem  22576  ordtuni  22578  idcn  22645  cnrmi  22748  cmpsublem  22787  cmpsub  22788  tgcmp  22789  uncmp  22791  hauscmplem  22794  cmpfi  22796  bwth  22798  1stcrestlem  22840  disllycmp  22886  dis1stc  22887  refref  22901  kgeni  22925  1stckgenlem  22941  kqffn  23113  snfil  23252  filconn  23271  cfinfil  23281  ufileu  23307  filufint  23308  fixufil  23310  cfinufil  23316  ufilen  23318  fin1aufil  23320  fmf  23333  rnelfm  23341  flimclslem  23372  hauspwpwf1  23375  supnfcls  23408  flimfnfcls  23416  fclscmp  23418  alexsubALTlem2  23436  alexsubALTlem3  23437  alexsubALT  23439  ptcmplem1  23440  cnextrel  23451  tsmsfbas  23516  ustref  23607  trust  23618  restutop  23626  isusp  23650  xmet0  23732  imasdsf1olem  23763  blfvalps  23773  blfps  23796  blf  23797  restmetu  23963  dscmet  23965  isngp2  23990  nm0  24022  nrginvrcn  24093  nmoix  24130  qdensere  24170  iccconn  24230  iccpnfcnv  24344  xrhmeo  24346  lebnumlem3  24363  metsscmetcld  24716  bcthlem5  24729  csschl  24777  rrxmfval  24807  minveclem3b  24829  cniccbdd  24862  ovolicc2lem4  24921  iunmbl  24954  ioorinv  24977  ioorcl  24978  i1f1lem  25090  limcvallem  25272  ellimc2  25278  limccnp  25292  limccnp2  25293  limcco  25294  perfdvf  25304  recnprss  25305  fncpn  25334  dvcmulf  25346  c1lip1  25398  lhop2  25416  q1pcl  25557  r1pdeglt  25560  ply1remlem  25564  plyssc  25598  ulm0  25787  cxpeq0  26070  cxplea  26088  cxplogb  26173  asinlem  26255  isppw2  26501  muval2  26520  dchrfi  26640  dchrpt  26652  bposlem6  26674  lgsdir2lem2  26711  lgsqr  26736  gausslemma2dlem4  26754  2lgslem2  26780  2lgslem3  26789  2lgs  26792  2sqlem7  26809  2sqlem11  26814  chtppilim  26860  nosgnn0i  27044  nolesgn2ores  27057  nogesgn1ores  27059  nosepnelem  27064  nosepdmlem  27068  nosupbnd1lem3  27095  nosupbnd1lem5  27097  nosupbnd2lem1  27100  noinfbnd1lem3  27110  noinfbnd1lem5  27112  noinfbnd2lem1  27115  oldval  27227  made0  27246  lrrecpo  27296  tgldimor  27507  tgcgr4  27536  tglnfn  27552  tglnunirn  27553  mirne  27672  mircinv  27673  perpln1  27715  perpln2  27716  lmiisolem  27801  xmstrkgc  27897  axcgrtr  27927  axsegconlem9  27937  axlowdimlem5  27958  axlowdimlem17  27970  axlowdim1  27971  uhgr0e  28085  edglnl  28157  uhgr0edgfi  28251  issubgr2  28283  subgrprop2  28285  egrsubgr  28288  0grsubgr  28289  0uhgrsubgr  28290  uhgrsubgrself  28291  nbgr0vtx  28367  nbgr1vtx  28369  nbgrssovtx  28372  nb3grprlem1  28391  uvtx01vtx  28408  cplgr1vlem  28440  cplgr1v  28441  usgrexilem  28451  wlkcomp  28642  wlk1walk  28650  wlkp1lem5  28688  uhgrwkspthlem1  28764  pthdlem1  28777  clwlkcomp  28790  lfgrn1cycl  28813  uspgrn2crct  28816  wwlksn0s  28869  umgrwwlks2on  28965  clwwlkn  29033  clwwlkn1  29048  0ewlk  29121  1ewlk  29122  0spth  29133  upgr1wlkdlem2  29153  wlk2v2e  29164  upgr3v3e3cycl  29187  upgr4cycl4dv4e  29192  eupth0  29221  frgr0v  29269  frgr1v  29278  1vwmgr  29283  ex-opab  29439  grpoinvf  29537  nvmid  29664  nmlnoubi  29801  hiidrcl  30100  hsn0elch  30253  shjshseli  30498  cmbr4i  30606  dfiop2  30758  kbpj  30961  nmopun  31019  adjeq0  31096  kbass2  31122  pjssdif1i  31180  pjinvari  31196  pjcmul2i  31207  pj3i  31213  stge1i  31243  stle0i  31244  sumdmdlem2  31424  dmdbr6ati  31428  dmdbr7ati  31429  rabsnel  31492  unidifsnel  31526  unidifsnne  31527  disjdifprg  31560  ofoprabco  31647  padct  31704  fpwrelmapffslem  31717  xrlelttric  31725  xnn0gt0  31742  iundisj2cnt  31770  f1ocnt  31773  fz1nnct  31774  fz1nntr  31775  hashxpe  31779  dvdszzq  31781  nn0min  31786  wrdt2ind  31877  xrge0tsmsbi  31970  locfinref  32511  dispcmp  32529  zartopn  32545  zarcmplem  32551  pstmxmet  32567  xrge0iifcnv  32603  xrge0iif1  32608  qqhre  32690  esumcl  32718  esumpr2  32755  esumpinfval  32761  esumpcvgval  32766  ofcfn  32788  pwsiga  32818  prsiga  32819  sigainb  32824  ldgenpisyslem1  32851  measiuns  32905  relfae  32935  pmeasmono  33013  sitgf  33036  eulerpartgbij  33061  sgnmulsgn  33238  sgnmulsgp  33239  signswch  33262  signslema  33263  signstlen  33268  signstfvn  33270  circlevma  33344  bnj216  33433  bnj151  33578  bnj517  33586  bnj970  33648  bnj1145  33694  bnj1498  33762  fineqvrep  33785  fineqvac  33787  0nn0m1nnn0  33792  pthhashvtx  33808  acycgr0v  33829  prclisacycgr  33832  umgracycusgr  33835  cusgracyclt3v  33837  subfacp1lem5  33865  erdszelem8  33879  kur14lem1  33887  indispconn  33915  cvmsss2  33955  satfvsuclem2  34041  satfrel  34048  satfrnmapom  34051  satfv0fun  34052  satf00  34055  satf0suclem  34056  fmlasuc0  34065  msubrn  34210  dfon2lem7  34450  brbigcup  34559  elsingles  34579  fnimage  34590  funpartlem  34603  dfrdg4  34612  imagesset  34614  altopthsn  34622  elaltxp  34636  ellines  34813  linethru  34814  rankeq1o  34832  elhf2  34836  hfninf  34847  nn0prpwlem  34870  fneref  34898  neibastop2lem  34908  limsucncmpi  34993  bj-exlimmpbir  35457  curryset  35490  bj-snglex  35517  bj-restpw  35636  bj-inftyexpidisj  35754  topdifinffinlem  35891  relowlssretop  35907  rdgeqoa  35914  finxpreclem6  35940  fvineqsneq  35956  pibt2  35961  poimirlem23  36174  poimirlem29  36180  poimirlem31  36182  volsupnfl  36196  cnambfre  36199  dvasin  36235  dvacos  36236  sdclem2  36274  sstotbnd2  36306  ssbnd  36320  ismgmOLD  36382  grpokerinj  36425  rngomndo  36467  isdrngo1  36488  ac6s6  36704  iss2  36878  cnvelrels  37030  cosselrels  37031  brssrid  37037  brcnvssrid  37042  dfdisjs5  37247  eldisjs5  37261  mpets2  37376  pets  37387  prtlem12  37402  riotasv2d  37492  lkrscss  37633  islshpkrN  37655  isline  38275  ispointN  38278  0psubN  38285  linepsubN  38288  atpsubN  38289  cdlemk36  39449  diafn  39570  dibfna  39690  dibvalrel  39699  dicvalrelN  39721  diclspsn  39730  dihvalrel  39815  dih1  39822  lclkrlem1  40042  lclkr  40069  mapd1o  40184  mapdin  40198  hdmapfnN  40365  hgmapfnN  40424  lcmineqlem10  40568  sticksstones9  40635  sn-iotalem  40714  repncan2  40909  sn-inelr  40992  elrfirn  41076  ismrcd1  41079  istopclsd  41081  rabren3dioph  41196  jm2.17b  41343  jm2.22  41377  jm2.23  41378  ttac  41418  pw2f1ocnv  41419  dnnumch1  41429  hbtlem5  41513  mncn0  41524  aaitgo  41547  rngunsnply  41558  unielss  41610  onexlimgt  41635  cantnfresb  41717  dflim5  41722  naddwordnexlem4  41795  safesnsupfiss  41809  safesnsupfidom1o  41811  safesnsupfilb  41812  ensucne0OLD  41924  clcnvlem  42017  relexp01min  42107  ntrf  42517  ssrecnpr  42710  seff  42711  sblpnf  42712  nzss  42719  dvconstbi  42736  ipo0  42851  ifr0  42852  addrfn  42874  subrfn  42875  mulvfn  42876  refsum2cnlem1  43364  rn1st  43623  ellimciota  43975  dvmptconst  44276  dvmptidg  44278  dvmulcncf  44286  dvdivcncf  44288  stoweidlem26  44387  stoweidlem50  44411  stoweidlem57  44418  aiotaval  45447  ndfatafv2nrn  45573  afv2ndefb  45576  funop1  45635  fun2dmnopgexmpl  45636  2ffzoeq  45680  iccpartiltu  45734  iccpartigtl  45735  zofldiv2ALTV  45974  evenprm2  46026  9fppr8  46049  stgoldbwt  46088  nnsum3primesle9  46106  nnsum4primeseven  46112  nnsum4primesevenALTV  46113  tgblthelfgott  46127  isomgreqve  46137  uspgrex  46172  0mgm  46188  nnsgrpmgm  46230  c0snmhm  46333  rngchomffvalALTV  46413  funcringcsetcALTV2lem4  46457  funcringcsetclem4ALTV  46480  srhmsubc  46494  rhmsubclem1  46504  srhmsubcALTV  46512  rhmsubcALTVlem1  46522  mapsnop  46540  zlmodzxzldeplem4  46704  zofldiv2  46737  fdivval  46745  nnlog2ge0lt1  46772  dig1  46814  itcoval2  46870  itcoval3  46871  mosn  47017  mo0  47018  mof02  47025  mofeu  47034  f102g  47038  f1mo  47039  f1omo  47047  intubeu  47129  unilbeu  47130  functhinclem1  47181  fullthinc  47186  thincciso  47189  indthinc  47192  indthincALT  47193