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  3308  raleleqOLD  3309  ceqsexv2d  3480  dedhb  3650  csbie2df  4384  ssdifeq0  4427  dedth  4526  pwidg  4562  snidg  4605  rexreusng  4624  exsnrex  4625  ifpr  4638  rmosn  4664  rabrsn  4669  prid1g  4705  tpid1g  4714  tpid2g  4716  tpid3g  4717  pwpw0  4757  sssn  4770  elpreqpr  4811  unimax  4888  intmin3  4919  eqbrtrdi  5125  al0ssb  5243  rabelpw  5271  intabs  5284  difelpw  5289  0inp0  5294  axpr  5362  intidg  5402  copsexgw  5436  copsexg  5437  euotd  5459  elopab  5473  elvvuni  5699  posn  5708  frsn  5710  eqrelriv  5736  relsnb  5749  relopabiALT  5770  opabid2  5775  ididg  5800  iss  5992  dfpo2  6252  ord0eln0  6371  sucidg  6398  nsuceq0  6400  funopg  6524  fn0  6621  f00  6714  f0bi  6715  f10d  6806  f1o00  6807  fo00  6808  brprcneu  6822  brprcneuALT  6823  dffn5  6890  fsn  7080  funop  7094  funsndifnop  7096  fnsnbOLD  7112  eufnfv  7175  f1ounsn  7218  f1eqcocnv  7247  nfriotadw  7323  nfriotad  7326  riotaprop  7342  oprabidw  7389  oprabid  7390  elrnmpo  7494  ov6g  7522  ovelrn  7534  caovmo  7595  offn  7635  caofinvl  7654  fr3nr  7717  onprc  7723  ordeleqon  7727  onint0  7736  0elsuc  7777  onuninsuci  7782  orduninsuc  7785  ordzsl  7787  onzsl  7788  tfinds  7802  limomss  7813  limom  7824  peano5  7835  xpexr  7860  eqop2  7976  opreuopreu  7978  1stconst  8041  2ndconst  8042  frxp2  8085  frxp3  8092  funsssuppss  8131  dftpos3  8185  dftpos4  8186  oawordeulem  8480  omwordi  8497  nnmwordi  8562  riiner  8728  ecopover  8759  map0g  8823  mapsnd  8825  elixpsn  8876  en0  8956  en0ALT  8957  en0r  8958  en1  8962  snfi  8981  fiprc  8982  sbthlem2  9017  sbthlem4  9019  sbthlem5  9020  0domg  9033  findcard  9089  findcard2  9090  nneneq  9131  sdom1  9151  1sdom2dom  9155  fineqvlem  9167  nfielex  9175  enp1i  9180  elfiun  9334  marypha1lem  9337  oicl  9435  oif  9436  oion  9442  hartogslem1  9448  hartogs  9450  wemapso2  9459  card2on  9460  0wdom  9476  brwdom2  9479  inf3lem6  9543  cantnflem3  9601  cantnflem4  9602  wemapwe  9607  cnfcom  9610  ssttrcl  9625  ttrclselem2  9636  tctr  9648  r1tr  9689  r1rankidb  9717  r1pw  9758  scottex  9798  scott0  9799  bnd2  9806  eldju2ndl  9837  tskwe  9863  oncard  9873  cardlim  9885  harsdom  9908  en2eleq  9919  dfac8alem  9940  cardaleph  10000  iunfictbso  10025  infmap2  10128  ackbij1lem18  10147  cff  10159  cfsuc  10168  cff1  10169  cflim2  10174  cfss  10176  sdom2en01  10213  infpssrlem4  10217  fin23lem7  10227  fin23lem11  10228  isfin2-2  10230  fin23lem26  10236  fin23lem19  10247  fin23lem17  10249  isf34lem2  10284  isf34lem4  10288  fin1a2lem6  10316  fin1a2lem10  10320  fin1a2lem12  10322  itunifn  10328  hsmexlem1  10337  axcc2lem  10347  dcomex  10358  axdc3lem4  10364  ondomon  10474  konigthlem  10480  pwcfsdom  10495  cfpwsdom  10496  axpowndlem3  10511  canth4  10559  canthnumlem  10560  canthwelem  10562  canthwe  10563  canthp1lem2  10565  pwfseqlem4  10574  pwfseqlem5  10575  gchaleph  10583  gch2  10587  winainflem  10605  0tsk  10667  rankcf  10689  tskcard  10693  gruina  10730  grutsk  10734  tskmid  10752  indpi  10819  nqereu  10841  mulcanenq  10872  recmulnq  10876  archnq  10892  ltsopr  10944  1ne0sr  11008  0idsr  11009  00sr  11011  leid  11231  lelttric  11242  divcan3  11824  divid  11829  div0  11831  lemul1a  11998  nn1suc  12185  nn0n0n1ge2b  12495  xnn0xr  12504  xnn0nemnf  12510  nn0lt10b  12580  nn0ind-raph  12618  elnn1uz2  12864  indstr2  12866  uzsupss  12879  rpnnen1lem4  12919  rpnnen1lem5  12920  xrnemnf  13057  xrnepnf  13058  mnfltxr  13067  xnn0n0n1ge2b  13072  xnn0ge0  13074  xrlttri  13079  xrlttr  13080  xrleid  13091  qbtwnxr  13141  xmullem2  13206  xlemul1a  13229  xrub  13253  reltxrnmnf  13284  ixxun  13303  xnn0xrge0  13448  fztpval  13529  fseq1p1m1  13541  elfznelfzob  13718  ltweuz  13912  fzfi  13923  fsuppmapnn0fiubex  13943  ser0f  14006  0exp  14048  faclbnd4lem1  14244  bcn1  14264  hashnemnf  14295  hashv01gt1  14296  hashsnle1  14368  hashgt12el2  14374  hashpw  14387  hashf1  14408  fz1isolem  14412  hash2prb  14423  hash3tpb  14446  0wrd0  14491  wrdlen1  14505  ccatvalfn  14532  eqs1  14564  wrdl1exs1  14565  swrdlen  14599  swrdwrdsymb  14614  swrdspsleq  14617  cats1un  14672  wrdind  14673  wrd2ind  14674  swrdccatin1  14676  repswsymballbi  14731  cshw1  14773  scshwfzeqfzo  14777  wrdl2exs2  14897  trclfvcotr  14960  relexp1g  14977  relexp0rel  14988  relexprelg  14989  relexpreld  14991  sqrt0  15192  sqrtsq  15220  mptfzshft  15729  prodf1f  15846  egt2lt3  16162  0dvds  16234  nn0onn  16338  nn0o  16341  divalgmod  16364  flodddiv4  16373  bitsp1o  16391  gcddvds  16461  bezout  16501  lcmdvds  16566  rpdvds  16618  1nprm  16637  prmind2  16643  dvdszzq  16680  nnoddn2prmb  16773  pcpre1  16802  vdwapf  16932  vdwapid1  16935  ram0  16982  ramz  16985  prmolefac  17006  cshws0  17061  prmlem0  17065  strle1  17117  restsspw  17383  prdsdsfn  17417  imasdsfn  17467  imasaddfnlem  17481  imasvscafn  17490  xpsfrnel  17515  isacs1i  17612  cidfn  17634  fnhomeqhomf  17646  comffn  17660  isoval  17721  sscres  17779  cofucl  17844  idffth  17891  ressffth  17896  cat1lem  18052  catcoppccl  18073  estrchomfn  18090  funcestrcsetclem4  18098  funcestrcsetclem7  18101  equivestrcsetc  18107  funcsetcestrclem4  18113  funcsetcestrclem7  18116  1stfcl  18152  2ndfcl  18153  prfcl  18158  evlfcl  18177  curf1cl  18183  curfcl  18187  hofcl  18214  yonedainv  18236  pospo  18298  lubfun  18305  glbfun  18318  joindmss  18332  meetdmss  18346  ipopos  18491  acsficl2d  18507  dirref  18556  mgmidcl  18623  mgmlrid  18624  ielefmnd  18844  smndex1basss  18865  smndex1n0mnd  18872  cntzssv  19292  idresperm  19350  symgvalstruct  19361  pmtrfmvdn0  19426  symggen  19434  psgnunilem1  19457  psgnprfval  19485  slwpgp  19577  frgpmhm  19729  frgpuptinv  19735  frgpup3lem  19741  gsumzoppg  19908  gsumcom2  19939  c0snmhm  20432  srhmsubc  20646  rhmsubclem1  20651  rrgsupp  20667  abv0  20789  zrhrhm  21499  psgnodpmr  21578  frlmphllem  21768  ellspd  21790  psrvscafval  21936  psrridm  21950  ltbwe  22031  psrbag0  22049  psrbagsn  22050  subrgascl  22053  psdmul  22141  mattpostpos  22428  mavmul0  22526  mavmul0g  22527  mdet0f1o  22567  m1detdiag  22571  m2detleiblem5  22599  m2detleiblem6  22600  m2detleiblem3  22603  m2detleiblem4  22604  maducoeval2  22614  d1mat2pmat  22713  chpmat1dlem  22809  chpmat1d  22810  baspartn  22928  eltg3  22936  topnex  22970  fctop  22978  cctop  22980  discld  23063  mretopd  23066  neipeltop  23103  neitr  23154  restcls  23155  ordtbaslem  23162  ordtuni  23164  idcn  23231  cnrmi  23334  cmpsublem  23373  cmpsub  23374  tgcmp  23375  uncmp  23377  hauscmplem  23380  cmpfi  23382  bwth  23384  1stcrestlem  23426  disllycmp  23472  dis1stc  23473  refref  23487  kgeni  23511  1stckgenlem  23527  kqffn  23699  snfil  23838  filconn  23857  cfinfil  23867  ufileu  23893  filufint  23894  fixufil  23896  cfinufil  23902  ufilen  23904  fin1aufil  23906  fmf  23919  rnelfm  23927  flimclslem  23958  hauspwpwf1  23961  supnfcls  23994  flimfnfcls  24002  fclscmp  24004  alexsubALTlem2  24022  alexsubALTlem3  24023  alexsubALT  24025  ptcmplem1  24026  cnextrel  24037  tsmsfbas  24102  ustref  24193  trust  24203  restutop  24211  isusp  24235  xmet0  24316  imasdsf1olem  24347  blfvalps  24357  blfps  24380  blf  24381  restmetu  24544  dscmet  24546  isngp2  24571  nm0  24603  nrginvrcn  24666  nmoix  24703  qdensere  24743  iccconn  24805  iccpnfcnv  24920  xrhmeo  24922  lebnumlem3  24939  metsscmetcld  25291  bcthlem5  25304  csschl  25352  rrxmfval  25382  minveclem3b  25404  cniccbdd  25437  ovolicc2lem4  25496  iunmbl  25529  ioorinv  25552  ioorcl  25553  i1f1lem  25665  limcvallem  25847  ellimc2  25853  limccnp  25867  limccnp2  25868  limcco  25869  perfdvf  25879  recnprss  25880  fncpn  25909  dvcmulf  25921  c1lip1  25974  lhop2  25992  q1pcl  26134  r1pdeglt  26137  ply1remlem  26142  plyssc  26177  ulm0  26371  cxpeq0  26658  cxplea  26676  cxplogb  26767  asinlem  26849  isppw2  27096  muval2  27115  dchrfi  27237  dchrpt  27249  bposlem6  27271  lgsdir2lem2  27308  lgsqr  27333  gausslemma2dlem4  27351  2lgslem2  27377  2lgslem3  27386  2lgs  27389  2sqlem7  27406  2sqlem11  27411  chtppilim  27457  nosgnn0i  27642  nolesgn2ores  27655  nogesgn1ores  27657  nosepnelem  27662  nosepdmlem  27666  nosupbnd1lem3  27693  nosupbnd1lem5  27695  nosupbnd2lem1  27698  noinfbnd1lem3  27708  noinfbnd1lem5  27710  noinfbnd2lem1  27713  oldval  27845  made0  27874  lrrecpo  27952  pncan2s  28085  divscan3d  28247  abssor  28257  om2noseqfo  28309  noseqrdglem  28316  noseqrdgfn  28317  noseqrdg0  28318  onsfi  28367  nohalf  28435  expsne0  28447  pw2divscan3d  28452  tgldimor  28589  tgcgr4  28618  tglnfn  28634  tglnunirn  28635  mirne  28754  mircinv  28755  perpln1  28797  perpln2  28798  lmiisolem  28883  xmstrkgc  28973  axcgrtr  29003  axsegconlem9  29013  axlowdimlem5  29034  axlowdimlem17  29046  axlowdim1  29047  uhgr0e  29159  edglnl  29231  uhgr0edgfi  29328  issubgr2  29360  subgrprop2  29362  egrsubgr  29365  0grsubgr  29366  0uhgrsubgr  29367  uhgrsubgrself  29368  nbgr1vtx  29446  nbgrssovtx  29449  nb3grprlem1  29468  uvtx01vtx  29485  cplgr1vlem  29517  cplgr1v  29518  usgrexilem  29528  wlkcomp  29719  wlk1walk  29727  wlkp1lem5  29764  uhgrwkspthlem1  29841  pthdlem1  29854  clwlkcomp  29867  lfgrn1cycl  29893  uspgrn2crct  29896  wwlksn0s  29949  usgrwwlks2on  30046  umgrwwlks2on  30047  clwwlkn  30116  clwwlkn1  30131  0ewlk  30204  1ewlk  30205  0spth  30216  upgr1wlkdlem2  30236  wlk2v2e  30247  upgr3v3e3cycl  30270  upgr4cycl4dv4e  30275  eupth0  30304  frgr0v  30352  frgr1v  30361  1vwmgr  30366  ex-opab  30522  grpoinvf  30623  nvmid  30750  nmlnoubi  30887  hiidrcl  31186  hsn0elch  31339  shjshseli  31584  cmbr4i  31692  dfiop2  31844  kbpj  32047  nmopun  32105  adjeq0  32182  kbass2  32208  pjssdif1i  32266  pjinvari  32282  pjcmul2i  32293  pj3i  32299  stge1i  32329  stle0i  32330  sumdmdlem2  32510  dmdbr6ati  32514  dmdbr7ati  32515  rabsnel  32590  unidifsnel  32625  unidifsnne  32626  disjdifprg  32665  ofoprabco  32757  padct  32811  fpwrelmapffslem  32825  nn0mnfxrd  32844  xrlelttric  32845  xnn0gt0  32862  iundisj2cnt  32892  f1ocnt  32893  fz1nnct  32894  fz1nntr  32895  hashxpe  32900  nn0min  32914  sgnmulsgn  32935  sgnmulsgp  32936  wrdt2ind  33033  xrge0tsmsbi  33155  opprabs  33562  rtelextdg2lem  33891  2sqr3minply  33945  locfinref  34006  dispcmp  34024  zartopn  34040  zarcmplem  34046  pstmxmet  34062  xrge0iifcnv  34098  xrge0iif1  34103  qqhre  34185  esumcl  34195  esumpr2  34232  esumpinfval  34238  esumpcvgval  34243  ofcfn  34265  pwsiga  34295  prsiga  34296  sigainb  34301  ldgenpisyslem1  34328  measiuns  34382  relfae  34412  pmeasmono  34489  sitgf  34512  eulerpartgbij  34537  signswch  34726  signslema  34727  signstlen  34732  signstfvn  34734  circlevma  34807  bnj216  34896  bnj151  35040  bnj517  35048  bnj970  35110  bnj1145  35156  bnj1498  35224  r1omhfb  35277  fineqvrep  35279  fineqvac  35281  fineqvnttrclselem1  35286  fineqvnttrclselem2  35287  fineqvnttrclse  35289  fineqvinfep  35290  r1omhfbregs  35302  wevgblacfn  35312  0nn0m1nnn0  35316  pthhashvtx  35331  acycgr0v  35351  prclisacycgr  35354  umgracycusgr  35357  cusgracyclt3v  35359  subfacp1lem5  35387  erdszelem8  35401  kur14lem1  35409  indispconn  35437  cvmsss2  35477  satfvsuclem2  35563  satfrel  35570  satfrnmapom  35573  satfv0fun  35574  satf00  35577  satf0suclem  35578  fmlasuc0  35587  msubrn  35732  dfon2lem7  35990  brbigcup  36099  elsingles  36119  fnimage  36130  funpartlem  36145  dfrdg4  36154  imagesset  36156  altopthsn  36164  elaltxp  36178  ellines  36355  linethru  36356  rankeq1o  36374  elhf2  36378  hfninf  36389  nn0prpwlem  36525  fneref  36553  neibastop2lem  36563  limsucncmpi  36648  tz9.1tco  36686  bj-exlimmpbir  37234  curryset  37266  bj-snglex  37293  bj-axnul  37392  bj-restpw  37417  bj-inftyexpidisj  37537  topdifinffinlem  37674  relowlssretop  37690  rdgeqoa  37697  finxpreclem6  37723  fvineqsneq  37739  pibt2  37744  poimirlem23  37975  poimirlem29  37981  poimirlem31  37983  volsupnfl  37997  cnambfre  38000  dvasin  38036  dvacos  38037  sdclem2  38074  sstotbnd2  38106  ssbnd  38120  ismgmOLD  38182  grpokerinj  38225  rngomndo  38267  isdrngo1  38288  ac6s6  38504  iss2  38676  relecxrn  38739  sucmapsuc  38821  cosselrels  38907  cnvelrels  38908  brssrid  38914  brcnvssrid  38919  dfdisjs5  39129  eldisjs5  39155  eldisjsim3  39269  mpets2  39287  pets  39298  prtlem12  39324  riotasv2d  39414  lkrscss  39555  islshpkrN  39577  isline  40196  ispointN  40199  0psubN  40206  linepsubN  40209  atpsubN  40210  cdlemk36  41370  diafn  41491  dibfna  41611  dibvalrel  41620  dicvalrelN  41642  diclspsn  41651  dihvalrel  41736  dih1  41743  lclkrlem1  41963  lclkr  41990  mapd1o  42105  mapdin  42119  hdmapfnN  42286  hgmapfnN  42345  lcmineqlem10  42488  sticksstones9  42604  sn-iotalem  42673  readvrec2  42804  readvrec  42805  repncan2  42825  elrfirn  43138  ismrcd1  43141  istopclsd  43143  rabren3dioph  43258  jm2.17b  43404  jm2.22  43438  jm2.23  43439  ttac  43479  pw2f1ocnv  43480  dnnumch1  43487  hbtlem5  43571  mncn0  43582  aaitgo  43605  rngunsnply  43612  unielss  43661  onexlimgt  43686  cantnfresb  43767  dflim5  43772  naddwordnexlem4  43844  safesnsupfiss  43857  safesnsupfidom1o  43859  safesnsupfilb  43860  ensucne0OLD  43972  clcnvlem  44065  relexp01min  44155  ntrf  44565  ssrecnpr  44750  seff  44751  sblpnf  44752  nzss  44759  dvconstbi  44776  ipo0  44890  ifr0  44891  addrfn  44913  subrfn  44914  mulvfn  44915  wfaxrep  45436  refsum2cnlem1  45483  rn1st  45717  ellimciota  46059  dvmptconst  46358  dvmptidg  46360  dvmulcncf  46368  dvdivcncf  46370  stoweidlem26  46469  stoweidlem50  46493  stoweidlem57  46500  aiotaval  47540  ndfatafv2nrn  47666  afv2ndefb  47669  funop1  47728  fun2dmnopgexmpl  47729  2ffzoeq  47773  2ltceilhalf  47777  m1modne  47799  iccpartiltu  47879  iccpartigtl  47880  zofldiv2ALTV  48135  evenprm2  48187  9fppr8  48210  stgoldbwt  48249  nnsum3primesle9  48267  nnsum4primeseven  48273  nnsum4primesevenALTV  48274  tgblthelfgott  48288  dfclnbgr6  48329  cycl3grtri  48420  grtrimap  48421  stgredgel  48430  stgr1  48434  isubgr3stgrlem2  48440  isubgr3stgrlem3  48441  usgrexmpl2trifr  48510  gpg5nbgrvtx13starlem1  48544  gpg5nbgrvtx13starlem2  48545  gpg5nbgrvtx13starlem3  48546  gpg5nbgr3star  48554  gpg3kgrtriex  48562  uspgrex  48623  0mgm  48639  nnsgrpmgm  48649  rngchomffvalALTV  48751  rhmsubcALTVlem1  48754  funcringcsetcALTV2lem4  48766  funcringcsetclem4ALTV  48789  srhmsubcALTV  48798  mapsnop  48817  zlmodzxzldeplem4  48976  zofldiv2  49004  fdivval  49012  nnlog2ge0lt1  49039  dig1  49081  itcoval2  49137  itcoval3  49138  mosn  49285  mo0  49286  mof02  49311  mofeu  49320  f102g  49324  f1mo  49325  tposres0  49349  f1omo  49365  f1omoOLD  49366  resipos  49447  intubeu  49456  unilbeu  49457  sectfn  49501  nelsubclem  49539  idfu1stf1o  49571  imaidfu  49582  oppfvallem  49607  funcoppc3  49619  idfth  49630  idsubc  49632  uptposlem  49669  swapf2fn  49740  swapf1f1o  49747  swapf2f1o  49748  swapf2f1oaALT  49750  fucof1  49794  fucofn2  49796  fucofn22  49812  reldmprcof1  49853  reldmprcof2  49854  fucoppcid  49880  fucoppc  49882  functhinclem1  49916  fullthinc  49922  thincciso  49925  indcthing  49932  indthinc  49934  indthincALT  49935  functermc  49980  discsntermlem  50042  reldmlan2  50089  reldmran2  50090  rellan  50095  relran  50096  termolmd  50142