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  1082  spei  2395  nfald2  2446  nfabd2  2934  raleleqALT  3358  dedhb  3640  sbceqalOLD  3784  csbie2df  4375  ssdifeq0  4418  r19.2zb  4427  dedth  4518  pwidg  4556  elpr2OLD  4588  snidg  4596  rexreusng  4616  exsnrex  4617  ifpr  4628  rmosn  4656  rabrsn  4661  prid1g  4697  tpid1g  4706  tpid2g  4708  tpid3g  4709  pwpw0  4747  sssn  4760  elpreqpr  4798  pwsnOLD  4833  unimax  4878  intmin3  4908  eqbrtrdi  5114  al0ssb  5233  intabs  5267  pwnss  5273  difelpw  5275  rabelpw  5276  0inp0  5282  copsexgw  5405  copsexg  5406  euotd  5428  elopab  5441  elvvuni  5664  posn  5673  frsn  5675  eqrelriv  5701  relsnb  5714  relopabiALT  5735  opabid2  5740  ididg  5765  iss  5946  dfpo2  6203  ord0eln0  6324  sucidg  6348  nsuceq0  6350  funopg  6475  fn0  6573  f00  6665  f0bi  6666  f10d  6759  f1o00  6760  fo00  6761  brprcneu  6773  brprcneuALT  6774  dffn5  6837  fsn  7016  funop  7030  funsndifnop  7032  fnsnb  7047  eufnfv  7114  f1eqcocnv  7182  f1eqcocnvOLD  7183  nfriotadw  7249  nfriotad  7253  riotaprop  7269  oprabidw  7315  oprabid  7316  elrnmpo  7419  ov6g  7445  ovelrn  7457  caovmo  7518  offn  7555  caofinvl  7572  fr3nr  7631  onprc  7637  ordeleqon  7641  onint0  7650  0elsuc  7691  onuninsuci  7696  orduninsuc  7699  ordzsl  7701  onzsl  7702  tfinds  7715  limomss  7726  limom  7737  peano5  7749  peano5OLD  7750  xpexr  7774  eqop2  7883  opreuopreu  7885  1stconst  7949  2ndconst  7950  funsssuppss  8015  dftpos3  8069  dftpos4  8070  wfrlem4OLD  8152  wfrlem14OLD  8162  oawordeulem  8394  omwordi  8411  nnmwordi  8475  riiner  8588  ecopover  8619  map0g  8681  mapsnd  8683  elixpsn  8734  en0  8812  en0OLD  8813  en0ALT  8814  en0r  8815  en1  8820  en1OLD  8821  fiprc  8844  sbthlem2  8880  sbthlem4  8882  sbthlem5  8883  0domg  8896  findcard  8955  findcard2  8956  nneneq  9001  nneneqOLD  9013  sdom1  9031  fineqvlem  9046  nfielex  9056  findcard2OLD  9065  elfiun  9198  marypha1lem  9201  oicl  9297  oif  9298  oion  9304  hartogslem1  9310  hartogs  9312  wemapso2  9321  card2on  9322  0wdom  9338  brwdom2  9341  inf3lem6  9400  cantnflem3  9458  cantnflem4  9459  wemapwe  9464  cnfcom  9467  ssttrcl  9482  ttrclselem2  9493  tctr  9507  r1tr  9543  r1rankidb  9571  r1pw  9612  scottex  9652  scott0  9653  bnd2  9660  eldju2ndl  9691  tskwe  9717  oncard  9727  cardlim  9739  harsdom  9762  en2eleq  9773  dfac8alem  9794  cardaleph  9854  iunfictbso  9879  infmap2  9983  ackbij1lem18  10002  cff  10013  cfsuc  10022  cff1  10023  cflim2  10028  cfss  10030  sdom2en01  10067  infpssrlem4  10071  fin23lem7  10081  fin23lem11  10082  isfin2-2  10084  fin23lem26  10090  fin23lem19  10101  fin23lem17  10103  isf34lem2  10138  isf34lem4  10142  fin1a2lem6  10170  fin1a2lem10  10174  fin1a2lem12  10176  itunifn  10182  hsmexlem1  10191  axcc2lem  10201  dcomex  10212  axdc3lem4  10218  ondomon  10328  konigthlem  10333  pwcfsdom  10348  cfpwsdom  10349  axpowndlem3  10364  canth4  10412  canthnumlem  10413  canthwelem  10415  canthwe  10416  canthp1lem2  10418  pwfseqlem4  10427  pwfseqlem5  10428  gchaleph  10436  gch2  10440  winainflem  10458  0tsk  10520  rankcf  10542  tskcard  10546  gruina  10583  grutsk  10587  tskmid  10605  indpi  10672  nqereu  10694  mulcanenq  10725  recmulnq  10729  archnq  10745  ltsopr  10797  1ne0sr  10861  0idsr  10862  00sr  10864  leid  11080  lelttric  11091  divcan3  11668  lemul1a  11838  nn1suc  12004  nn0n0n1ge2b  12310  xnn0xr  12319  xnn0nemnf  12325  nn0lt10b  12391  nn0ind-raph  12429  elnn1uz2  12674  indstr2  12676  uzsupss  12689  rpnnen1lem4  12729  rpnnen1lem5  12730  xrnemnf  12862  xrnepnf  12863  mnfltxr  12872  xnn0n0n1ge2b  12876  xnn0ge0  12878  xrlttri  12882  xrlttr  12883  xrleid  12894  qbtwnxr  12943  xmullem2  13008  xlemul1a  13031  xrub  13055  reltxrnmnf  13085  ixxun  13104  xnn0xrge0  13247  fztpval  13327  fseq1p1m1  13339  elfznelfzob  13502  ltweuz  13690  fzfi  13701  fsuppmapnn0fiubex  13721  ser0f  13785  0exp  13827  faclbnd4lem1  14016  bcn1  14036  hashnemnf  14067  hashv01gt1  14068  hashsnle1  14141  hashgt12el2  14147  hashpw  14160  hashf1  14180  fz1isolem  14184  hash2prb  14195  0wrd0  14252  wrdlen1  14266  ccatvalfn  14295  eqs1  14326  wrdl1exs1  14327  swrdlen  14369  swrdwrdsymb  14384  swrdspsleq  14387  cats1un  14443  wrdind  14444  wrd2ind  14445  swrdccatin1  14447  repswsymballbi  14502  cshw1  14544  scshwfzeqfzo  14548  wrdl2exs2  14668  trclfvcotr  14729  relexp1g  14746  relexp0rel  14757  relexprelg  14758  relexpreld  14760  sqr0lem  14961  sqrtsq  14990  mptfzshft  15499  prodf1f  15613  egt2lt3  15924  0dvds  15995  nn0onn  16098  nn0o  16101  divalgmod  16124  flodddiv4  16131  bitsp1o  16149  gcddvds  16219  bezout  16260  lcmdvds  16322  rpdvds  16374  1nprm  16393  prmind2  16399  nnoddn2prmb  16523  pcpre1  16552  vdwapf  16682  vdwapid1  16685  ram0  16732  ramz  16735  prmolefac  16756  cshws0  16812  prmlem0  16816  strle1  16868  restsspw  17151  prdsdsfn  17185  imasdsfn  17234  imasaddfnlem  17248  imasvscafn  17257  xpsfrnel  17282  isacs1i  17375  cidfn  17397  fnhomeqhomf  17409  comffn  17423  isoval  17486  sscres  17544  cofucl  17612  idffth  17658  ressffth  17663  cat1lem  17820  catcoppccl  17841  catcoppcclOLD  17842  estrchomfn  17860  funcestrcsetclem4  17869  funcestrcsetclem7  17872  equivestrcsetc  17878  funcsetcestrclem4  17884  funcsetcestrclem7  17887  1stfcl  17923  2ndfcl  17924  prfcl  17929  evlfcl  17949  curf1cl  17955  curfcl  17959  hofcl  17986  yonedainv  18008  pospo  18072  lubfun  18079  glbfun  18092  joindmss  18106  meetdmss  18120  ipopos  18263  acsficl2d  18279  dirref  18328  mgmidcl  18359  mgmlrid  18360  ielefmnd  18535  smndex1basss  18553  smndex1n0mnd  18560  cntzssv  18943  idresperm  19002  symgvalstruct  19013  symgvalstructOLD  19014  pmtrfmvdn0  19079  symggen  19087  psgnunilem1  19110  psgnprfval  19138  slwpgp  19227  frgpmhm  19380  frgpuptinv  19386  frgpup3lem  19392  gsumzoppg  19554  gsumcom2  19585  abv0  20100  rrgsupp  20571  zrhrhm  20722  psgnodpmr  20804  frlmphllem  20996  frlmphl  20997  ellspd  21018  psrvscafval  21168  psrridm  21182  ltbwe  21254  psrbag0  21279  psrbagsn  21280  subrgascl  21283  mattpostpos  21612  mavmul0  21710  mavmul0g  21711  mdet0f1o  21751  m1detdiag  21755  m2detleiblem5  21783  m2detleiblem6  21784  m2detleiblem3  21787  m2detleiblem4  21788  maducoeval2  21798  d1mat2pmat  21897  chpmat1dlem  21993  chpmat1d  21994  baspartn  22113  eltg3  22121  topnex  22155  fctop  22163  cctop  22165  discld  22249  mretopd  22252  neipeltop  22289  neitr  22340  restcls  22341  ordtbaslem  22348  ordtuni  22350  idcn  22417  cnrmi  22520  cmpsublem  22559  cmpsub  22560  tgcmp  22561  uncmp  22563  hauscmplem  22566  cmpfi  22568  bwth  22570  1stcrestlem  22612  disllycmp  22658  dis1stc  22659  refref  22673  kgeni  22697  1stckgenlem  22713  kqffn  22885  snfil  23024  filconn  23043  cfinfil  23053  ufileu  23079  filufint  23080  fixufil  23082  cfinufil  23088  ufilen  23090  fin1aufil  23092  fmf  23105  rnelfm  23113  flimclslem  23144  hauspwpwf1  23147  supnfcls  23180  flimfnfcls  23188  fclscmp  23190  alexsubALTlem2  23208  alexsubALTlem3  23209  alexsubALT  23211  ptcmplem1  23212  cnextrel  23223  tsmsfbas  23288  ustref  23379  trust  23390  restutop  23398  isusp  23422  xmet0  23504  imasdsf1olem  23535  blfvalps  23545  blfps  23568  blf  23569  restmetu  23735  dscmet  23737  isngp2  23762  nm0  23794  nrginvrcn  23865  nmoix  23902  qdensere  23942  iccconn  24002  iccpnfcnv  24116  xrhmeo  24118  lebnumlem3  24135  metsscmetcld  24488  bcthlem5  24501  csschl  24549  rrxmfval  24579  minveclem3b  24601  cniccbdd  24634  ovolicc2lem4  24693  iunmbl  24726  ioorinv  24749  ioorcl  24750  i1f1lem  24862  limcvallem  25044  ellimc2  25050  limccnp  25064  limccnp2  25065  limcco  25066  perfdvf  25076  recnprss  25077  fncpn  25106  dvcmulf  25118  c1lip1  25170  lhop2  25188  q1pcl  25329  r1pdeglt  25332  ply1remlem  25336  plyssc  25370  ulm0  25559  cxpeq0  25842  cxplea  25860  cxplogb  25945  asinlem  26027  isppw2  26273  muval2  26292  dchrfi  26412  dchrpt  26424  bposlem6  26446  lgsdir2lem2  26483  lgsqr  26508  gausslemma2dlem4  26526  2lgslem2  26552  2lgslem3  26561  2lgs  26564  2sqlem7  26581  2sqlem11  26586  chtppilim  26632  tgldimor  26872  tgcgr4  26901  tglnfn  26917  tglnunirn  26918  mirne  27037  mircinv  27038  perpln1  27080  perpln2  27081  lmiisolem  27166  xmstrkgc  27262  axcgrtr  27292  axsegconlem9  27302  axlowdimlem5  27323  axlowdimlem17  27335  axlowdim1  27336  uhgr0e  27450  edglnl  27522  uhgr0edgfi  27616  issubgr2  27648  subgrprop2  27650  egrsubgr  27653  0grsubgr  27654  0uhgrsubgr  27655  uhgrsubgrself  27656  nbgr0vtx  27732  nbgr1vtx  27734  nbgrssovtx  27737  nb3grprlem1  27756  uvtx01vtx  27773  cplgr1vlem  27805  cplgr1v  27806  usgrexilem  27816  wlkcomp  28007  wlk1walk  28015  wlkp1lem5  28054  uhgrwkspthlem1  28130  pthdlem1  28143  clwlkcomp  28156  lfgrn1cycl  28179  uspgrn2crct  28182  wwlksn0s  28235  umgrwwlks2on  28331  clwwlkn  28399  clwwlkn1  28414  0ewlk  28487  1ewlk  28488  0spth  28499  upgr1wlkdlem2  28519  wlk2v2e  28530  upgr3v3e3cycl  28553  upgr4cycl4dv4e  28558  eupth0  28587  frgr0v  28635  frgr1v  28644  1vwmgr  28649  ex-opab  28805  grpoinvf  28903  nvmid  29030  nmlnoubi  29167  hiidrcl  29466  hsn0elch  29619  shjshseli  29864  cmbr4i  29972  dfiop2  30124  kbpj  30327  nmopun  30385  adjeq0  30462  kbass2  30488  pjssdif1i  30546  pjinvari  30562  pjcmul2i  30573  pj3i  30579  stge1i  30609  stle0i  30610  sumdmdlem2  30790  dmdbr6ati  30794  dmdbr7ati  30795  rabsnel  30856  unidifsnel  30892  unidifsnne  30893  disjdifprg  30923  ofoprabco  31010  padct  31063  fpwrelmapffslem  31076  xrlelttric  31084  xnn0gt0  31101  iundisj2cnt  31129  f1ocnt  31132  fz1nnct  31133  fz1nntr  31134  hashxpe  31136  dvdszzq  31138  nn0min  31143  wrdt2ind  31234  xrge0tsmsbi  31327  locfinref  31800  dispcmp  31818  zartopn  31834  zarcmplem  31840  pstmxmet  31856  xrge0iifcnv  31892  xrge0iif1  31897  qqhre  31979  esumcl  32007  esumpr2  32044  esumpinfval  32050  esumpcvgval  32055  ofcfn  32077  pwsiga  32107  prsiga  32108  sigainb  32113  ldgenpisyslem1  32140  measiuns  32194  relfae  32224  pmeasmono  32300  sitgf  32323  eulerpartgbij  32348  sgnmulsgn  32525  sgnmulsgp  32526  signswch  32549  signslema  32550  signstlen  32555  signstfvn  32557  circlevma  32631  bnj216  32720  bnj151  32866  bnj517  32874  bnj970  32936  bnj1145  32982  bnj1498  33050  fineqvrep  33073  fineqvac  33075  0nn0m1nnn0  33080  pthhashvtx  33098  acycgr0v  33119  prclisacycgr  33122  umgracycusgr  33125  cusgracyclt3v  33127  subfacp1lem5  33155  erdszelem8  33169  kur14lem1  33177  indispconn  33205  cvmsss2  33245  satfvsuclem2  33331  satfrel  33338  satfrnmapom  33341  satfv0fun  33342  satf00  33345  satf0suclem  33346  fmlasuc0  33355  msubrn  33500  dfon2lem7  33774  frxp2  33800  frxp3  33806  nosgnn0i  33871  nolesgn2ores  33884  nogesgn1ores  33886  nosepnelem  33891  nosepdmlem  33895  nosupbnd1lem3  33922  nosupbnd1lem5  33924  nosupbnd2lem1  33927  noinfbnd1lem3  33937  noinfbnd1lem5  33939  noinfbnd2lem1  33942  oldval  34047  made0  34066  lrrecpo  34107  brbigcup  34209  elsingles  34229  fnimage  34240  funpartlem  34253  dfrdg4  34262  imagesset  34264  altopthsn  34272  elaltxp  34286  ellines  34463  linethru  34464  rankeq1o  34482  elhf2  34486  hfninf  34497  nn0prpwlem  34520  fneref  34548  neibastop2lem  34558  limsucncmpi  34643  bj-exlimmpbir  35108  curryset  35144  bj-snglex  35172  bj-restpw  35272  bj-inftyexpidisj  35390  topdifinffinlem  35527  relowlssretop  35543  rdgeqoa  35550  finxpreclem6  35576  fvineqsneq  35592  pibt2  35597  poimirlem23  35809  poimirlem29  35815  poimirlem31  35817  volsupnfl  35831  cnambfre  35834  dvasin  35870  dvacos  35871  sdclem2  35909  sstotbnd2  35941  ssbnd  35955  ismgmOLD  36017  grpokerinj  36060  rngomndo  36102  isdrngo1  36123  ac6s6  36339  iss2  36486  cnvelrels  36620  cosselrels  36621  brssrid  36627  brcnvssrid  36632  dfdisjs5  36830  eldisjs5  36844  prtlem12  36888  riotasv2d  36978  lkrscss  37119  islshpkrN  37141  isline  37760  ispointN  37763  0psubN  37770  linepsubN  37773  atpsubN  37774  cdlemk36  38934  diafn  39055  dibfna  39175  dibvalrel  39184  dicvalrelN  39206  diclspsn  39215  dihvalrel  39300  dih1  39307  lclkrlem1  39527  lclkr  39554  mapd1o  39669  mapdin  39683  hdmapfnN  39850  hgmapfnN  39909  lcmineqlem10  40053  sticksstones9  40117  sn-iotalem  40196  repncan2  40372  sn-inelr  40442  prjcrv0  40477  elrfirn  40524  ismrcd1  40527  istopclsd  40529  rabren3dioph  40644  jm2.17b  40790  jm2.22  40824  jm2.23  40825  ttac  40865  pw2f1ocnv  40866  dnnumch1  40876  hbtlem5  40960  mncn0  40971  aaitgo  40994  rngunsnply  41005  ensucne0OLD  41144  clcnvlem  41238  relexp01min  41328  ntrf  41740  ssrecnpr  41933  seff  41934  sblpnf  41935  nzss  41942  dvconstbi  41959  ipo0  42074  ifr0  42075  addrfn  42097  subrfn  42098  mulvfn  42099  refsum2cnlem1  42587  ellimciota  43162  dvmptconst  43463  dvmptidg  43465  dvmulcncf  43473  dvdivcncf  43475  stoweidlem26  43574  stoweidlem50  43598  stoweidlem57  43605  aiotaval  44598  ndfatafv2nrn  44724  afv2ndefb  44727  funop1  44786  fun2dmnopgexmpl  44787  2ffzoeq  44831  iccpartiltu  44885  iccpartigtl  44886  zofldiv2ALTV  45125  evenprm2  45177  9fppr8  45200  stgoldbwt  45239  nnsum3primesle9  45257  nnsum4primeseven  45263  nnsum4primesevenALTV  45264  tgblthelfgott  45278  isomgreqve  45288  uspgrex  45323  0mgm  45339  nnsgrpmgm  45381  c0snmhm  45484  rngchomffvalALTV  45564  funcringcsetcALTV2lem4  45608  funcringcsetclem4ALTV  45631  srhmsubc  45645  rhmsubclem1  45655  srhmsubcALTV  45663  rhmsubcALTVlem1  45673  mapsnop  45691  zlmodzxzldeplem4  45855  zofldiv2  45888  fdivval  45896  nnlog2ge0lt1  45923  dig1  45965  itcoval2  46021  itcoval3  46022  mosn  46169  mo0  46170  mof02  46177  mofeu  46186  f102g  46190  f1mo  46191  f1omo  46199  intubeu  46281  unilbeu  46282  functhinclem1  46333  fullthinc  46338  thincciso  46341  indthinc  46344  indthincALT  46345