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  3306  raleleqOLD  3307  ceqsexv2d  3486  dedhb  3660  csbie2df  4391  ssdifeq0  4435  r19.2zb  4444  dedth  4532  pwidg  4568  snidg  4611  rexreusng  4630  exsnrex  4631  ifpr  4644  rmosn  4670  rabrsn  4675  prid1g  4711  tpid1g  4720  tpid2g  4722  tpid3g  4723  pwpw0  4763  sssn  4776  elpreqpr  4817  unimax  4893  intmin3  4924  eqbrtrdi  5128  al0ssb  5244  rabelpw  5272  intabs  5285  difelpw  5290  0inp0  5295  axpr  5363  intidg  5396  copsexgw  5428  copsexg  5429  euotd  5451  elopab  5465  elvvuni  5691  posn  5700  frsn  5702  eqrelriv  5727  relsnb  5740  relopabiALT  5761  opabid2  5766  ididg  5791  iss  5981  dfpo2  6239  ord0eln0  6358  sucidg  6385  nsuceq0  6387  funopg  6511  fn0  6608  f00  6701  f0bi  6702  f10d  6793  f1o00  6794  fo00  6795  brprcneu  6807  brprcneuALT  6808  dffn5  6875  fsn  7063  funop  7077  funsndifnop  7079  fnsnbOLD  7095  eufnfv  7158  f1ounsn  7201  f1eqcocnv  7230  nfriotadw  7306  nfriotad  7309  riotaprop  7325  oprabidw  7372  oprabid  7373  elrnmpo  7477  ov6g  7505  ovelrn  7517  caovmo  7578  offn  7618  caofinvl  7637  fr3nr  7700  onprc  7706  ordeleqon  7710  onint0  7719  0elsuc  7760  onuninsuci  7765  orduninsuc  7768  ordzsl  7770  onzsl  7771  tfinds  7785  limomss  7796  limom  7807  peano5  7818  xpexr  7843  eqop2  7959  opreuopreu  7961  1stconst  8025  2ndconst  8026  frxp2  8069  frxp3  8076  funsssuppss  8115  dftpos3  8169  dftpos4  8170  oawordeulem  8464  omwordi  8481  nnmwordi  8545  riiner  8709  ecopover  8740  map0g  8803  mapsnd  8805  elixpsn  8856  en0  8935  en0ALT  8936  en0r  8937  en1  8941  snfi  8960  fiprc  8961  sbthlem2  8996  sbthlem4  8998  sbthlem5  8999  0domg  9012  findcard  9068  findcard2  9069  nneneq  9110  sdom1  9129  1sdom2dom  9133  fineqvlem  9145  nfielex  9153  enp1i  9158  elfiun  9309  marypha1lem  9312  oicl  9410  oif  9411  oion  9417  hartogslem1  9423  hartogs  9425  wemapso2  9434  card2on  9435  0wdom  9451  brwdom2  9454  inf3lem6  9518  cantnflem3  9576  cantnflem4  9577  wemapwe  9582  cnfcom  9585  ssttrcl  9600  ttrclselem2  9611  tctr  9625  r1tr  9661  r1rankidb  9689  r1pw  9730  scottex  9770  scott0  9771  bnd2  9778  eldju2ndl  9809  tskwe  9835  oncard  9845  cardlim  9857  harsdom  9880  en2eleq  9891  dfac8alem  9912  cardaleph  9972  iunfictbso  9997  infmap2  10100  ackbij1lem18  10119  cff  10131  cfsuc  10140  cff1  10141  cflim2  10146  cfss  10148  sdom2en01  10185  infpssrlem4  10189  fin23lem7  10199  fin23lem11  10200  isfin2-2  10202  fin23lem26  10208  fin23lem19  10219  fin23lem17  10221  isf34lem2  10256  isf34lem4  10260  fin1a2lem6  10288  fin1a2lem10  10292  fin1a2lem12  10294  itunifn  10300  hsmexlem1  10309  axcc2lem  10319  dcomex  10330  axdc3lem4  10336  ondomon  10446  konigthlem  10451  pwcfsdom  10466  cfpwsdom  10467  axpowndlem3  10482  canth4  10530  canthnumlem  10531  canthwelem  10533  canthwe  10534  canthp1lem2  10536  pwfseqlem4  10545  pwfseqlem5  10546  gchaleph  10554  gch2  10558  winainflem  10576  0tsk  10638  rankcf  10660  tskcard  10664  gruina  10701  grutsk  10705  tskmid  10723  indpi  10790  nqereu  10812  mulcanenq  10843  recmulnq  10847  archnq  10863  ltsopr  10915  1ne0sr  10979  0idsr  10980  00sr  10982  leid  11201  lelttric  11212  divcan3  11794  divid  11799  div0  11801  lemul1a  11967  nn1suc  12139  nn0n0n1ge2b  12442  xnn0xr  12451  xnn0nemnf  12457  nn0lt10b  12527  nn0ind-raph  12565  elnn1uz2  12815  indstr2  12817  uzsupss  12830  rpnnen1lem4  12870  rpnnen1lem5  12871  xrnemnf  13008  xrnepnf  13009  mnfltxr  13018  xnn0n0n1ge2b  13023  xnn0ge0  13025  xrlttri  13030  xrlttr  13031  xrleid  13042  qbtwnxr  13091  xmullem2  13156  xlemul1a  13179  xrub  13203  reltxrnmnf  13234  ixxun  13253  xnn0xrge0  13398  fztpval  13478  fseq1p1m1  13490  elfznelfzob  13666  ltweuz  13860  fzfi  13871  fsuppmapnn0fiubex  13891  ser0f  13954  0exp  13996  faclbnd4lem1  14192  bcn1  14212  hashnemnf  14243  hashv01gt1  14244  hashsnle1  14316  hashgt12el2  14322  hashpw  14335  hashf1  14356  fz1isolem  14360  hash2prb  14371  hash3tpb  14394  0wrd0  14439  wrdlen1  14453  ccatvalfn  14480  eqs1  14512  wrdl1exs1  14513  swrdlen  14547  swrdwrdsymb  14562  swrdspsleq  14565  cats1un  14620  wrdind  14621  wrd2ind  14622  swrdccatin1  14624  repswsymballbi  14679  cshw1  14721  scshwfzeqfzo  14725  wrdl2exs2  14845  trclfvcotr  14908  relexp1g  14925  relexp0rel  14936  relexprelg  14937  relexpreld  14939  sqrt0  15140  sqrtsq  15168  mptfzshft  15677  prodf1f  15791  egt2lt3  16107  0dvds  16179  nn0onn  16283  nn0o  16286  divalgmod  16309  flodddiv4  16318  bitsp1o  16336  gcddvds  16406  bezout  16446  lcmdvds  16511  rpdvds  16563  1nprm  16582  prmind2  16588  dvdszzq  16624  nnoddn2prmb  16717  pcpre1  16746  vdwapf  16876  vdwapid1  16879  ram0  16926  ramz  16929  prmolefac  16950  cshws0  17005  prmlem0  17009  strle1  17061  restsspw  17327  prdsdsfn  17361  imasdsfn  17410  imasaddfnlem  17424  imasvscafn  17433  xpsfrnel  17458  isacs1i  17555  cidfn  17577  fnhomeqhomf  17589  comffn  17603  isoval  17664  sscres  17722  cofucl  17787  idffth  17834  ressffth  17839  cat1lem  17995  catcoppccl  18016  estrchomfn  18033  funcestrcsetclem4  18041  funcestrcsetclem7  18044  equivestrcsetc  18050  funcsetcestrclem4  18056  funcsetcestrclem7  18059  1stfcl  18095  2ndfcl  18096  prfcl  18101  evlfcl  18120  curf1cl  18126  curfcl  18130  hofcl  18157  yonedainv  18179  pospo  18241  lubfun  18248  glbfun  18261  joindmss  18275  meetdmss  18289  ipopos  18434  acsficl2d  18450  dirref  18499  mgmidcl  18566  mgmlrid  18567  ielefmnd  18787  smndex1basss  18805  smndex1n0mnd  18812  cntzssv  19233  idresperm  19291  symgvalstruct  19302  pmtrfmvdn0  19367  symggen  19375  psgnunilem1  19398  psgnprfval  19426  slwpgp  19518  frgpmhm  19670  frgpuptinv  19676  frgpup3lem  19682  gsumzoppg  19849  gsumcom2  19880  c0snmhm  20374  srhmsubc  20588  rhmsubclem1  20593  rrgsupp  20609  abv0  20731  zrhrhm  21441  psgnodpmr  21520  frlmphllem  21710  ellspd  21732  psrvscafval  21878  psrridm  21893  ltbwe  21972  psrbag0  21990  psrbagsn  21991  subrgascl  21994  psdmul  22074  mattpostpos  22362  mavmul0  22460  mavmul0g  22461  mdet0f1o  22501  m1detdiag  22505  m2detleiblem5  22533  m2detleiblem6  22534  m2detleiblem3  22537  m2detleiblem4  22538  maducoeval2  22548  d1mat2pmat  22647  chpmat1dlem  22743  chpmat1d  22744  baspartn  22862  eltg3  22870  topnex  22904  fctop  22912  cctop  22914  discld  22997  mretopd  23000  neipeltop  23037  neitr  23088  restcls  23089  ordtbaslem  23096  ordtuni  23098  idcn  23165  cnrmi  23268  cmpsublem  23307  cmpsub  23308  tgcmp  23309  uncmp  23311  hauscmplem  23314  cmpfi  23316  bwth  23318  1stcrestlem  23360  disllycmp  23406  dis1stc  23407  refref  23421  kgeni  23445  1stckgenlem  23461  kqffn  23633  snfil  23772  filconn  23791  cfinfil  23801  ufileu  23827  filufint  23828  fixufil  23830  cfinufil  23836  ufilen  23838  fin1aufil  23840  fmf  23853  rnelfm  23861  flimclslem  23892  hauspwpwf1  23895  supnfcls  23928  flimfnfcls  23936  fclscmp  23938  alexsubALTlem2  23956  alexsubALTlem3  23957  alexsubALT  23959  ptcmplem1  23960  cnextrel  23971  tsmsfbas  24036  ustref  24127  trust  24137  restutop  24145  isusp  24169  xmet0  24250  imasdsf1olem  24281  blfvalps  24291  blfps  24314  blf  24315  restmetu  24478  dscmet  24480  isngp2  24505  nm0  24537  nrginvrcn  24600  nmoix  24637  qdensere  24677  iccconn  24739  iccpnfcnv  24862  xrhmeo  24864  lebnumlem3  24882  metsscmetcld  25235  bcthlem5  25248  csschl  25296  rrxmfval  25326  minveclem3b  25348  cniccbdd  25382  ovolicc2lem4  25441  iunmbl  25474  ioorinv  25497  ioorcl  25498  i1f1lem  25610  limcvallem  25792  ellimc2  25798  limccnp  25812  limccnp2  25813  limcco  25814  perfdvf  25824  recnprss  25825  fncpn  25855  dvcmulf  25868  c1lip1  25922  lhop2  25940  q1pcl  26082  r1pdeglt  26085  ply1remlem  26090  plyssc  26125  ulm0  26320  cxpeq0  26607  cxplea  26625  cxplogb  26716  asinlem  26798  isppw2  27045  muval2  27064  dchrfi  27186  dchrpt  27198  bposlem6  27220  lgsdir2lem2  27257  lgsqr  27282  gausslemma2dlem4  27300  2lgslem2  27326  2lgslem3  27335  2lgs  27338  2sqlem7  27355  2sqlem11  27360  chtppilim  27406  nosgnn0i  27591  nolesgn2ores  27604  nogesgn1ores  27606  nosepnelem  27611  nosepdmlem  27615  nosupbnd1lem3  27642  nosupbnd1lem5  27644  nosupbnd2lem1  27647  noinfbnd1lem3  27657  noinfbnd1lem5  27659  noinfbnd2lem1  27662  oldval  27788  made0  27811  lrrecpo  27877  pncan2s  28007  divscan3d  28167  abssor  28177  om2noseqfo  28221  noseqrdglem  28228  noseqrdgfn  28229  noseqrdg0  28230  onsfi  28276  nohalf  28340  expsne0  28352  pw2divscan3d  28357  tgldimor  28473  tgcgr4  28502  tglnfn  28518  tglnunirn  28519  mirne  28638  mircinv  28639  perpln1  28681  perpln2  28682  lmiisolem  28767  xmstrkgc  28857  axcgrtr  28886  axsegconlem9  28896  axlowdimlem5  28917  axlowdimlem17  28929  axlowdim1  28930  uhgr0e  29042  edglnl  29114  uhgr0edgfi  29211  issubgr2  29243  subgrprop2  29245  egrsubgr  29248  0grsubgr  29249  0uhgrsubgr  29250  uhgrsubgrself  29251  nbgr1vtx  29329  nbgrssovtx  29332  nb3grprlem1  29351  uvtx01vtx  29368  cplgr1vlem  29400  cplgr1v  29401  usgrexilem  29411  wlkcomp  29602  wlk1walk  29610  wlkp1lem5  29647  uhgrwkspthlem1  29724  pthdlem1  29737  clwlkcomp  29750  lfgrn1cycl  29776  uspgrn2crct  29779  wwlksn0s  29832  umgrwwlks2on  29928  clwwlkn  29996  clwwlkn1  30011  0ewlk  30084  1ewlk  30085  0spth  30096  upgr1wlkdlem2  30116  wlk2v2e  30127  upgr3v3e3cycl  30150  upgr4cycl4dv4e  30155  eupth0  30184  frgr0v  30232  frgr1v  30241  1vwmgr  30246  ex-opab  30402  grpoinvf  30502  nvmid  30629  nmlnoubi  30766  hiidrcl  31065  hsn0elch  31218  shjshseli  31463  cmbr4i  31571  dfiop2  31723  kbpj  31926  nmopun  31984  adjeq0  32061  kbass2  32087  pjssdif1i  32145  pjinvari  32161  pjcmul2i  32172  pj3i  32178  stge1i  32208  stle0i  32209  sumdmdlem2  32389  dmdbr6ati  32393  dmdbr7ati  32394  rabsnel  32470  unidifsnel  32505  unidifsnne  32506  disjdifprg  32545  ofoprabco  32636  padct  32691  fpwrelmapffslem  32705  xrlelttric  32725  xnn0gt0  32742  iundisj2cnt  32771  f1ocnt  32772  fz1nnct  32773  fz1nntr  32774  hashxpe  32779  nn0min  32793  sgnmulsgn  32815  sgnmulsgp  32816  wrdt2ind  32924  xrge0tsmsbi  33033  opprabs  33437  rtelextdg2lem  33729  2sqr3minply  33783  locfinref  33844  dispcmp  33862  zartopn  33878  zarcmplem  33884  pstmxmet  33900  xrge0iifcnv  33936  xrge0iif1  33941  qqhre  34023  esumcl  34033  esumpr2  34070  esumpinfval  34076  esumpcvgval  34081  ofcfn  34103  pwsiga  34133  prsiga  34134  sigainb  34139  ldgenpisyslem1  34166  measiuns  34220  relfae  34250  pmeasmono  34327  sitgf  34350  eulerpartgbij  34375  signswch  34564  signslema  34565  signstlen  34570  signstfvn  34572  circlevma  34645  bnj216  34734  bnj151  34879  bnj517  34887  bnj970  34949  bnj1145  34995  bnj1498  35063  fineqvrep  35105  fineqvac  35107  fineqvnttrclselem1  35109  fineqvnttrclselem2  35110  fineqvnttrclse  35112  wevgblacfn  35121  0nn0m1nnn0  35125  pthhashvtx  35140  acycgr0v  35160  prclisacycgr  35163  umgracycusgr  35166  cusgracyclt3v  35168  subfacp1lem5  35196  erdszelem8  35210  kur14lem1  35218  indispconn  35246  cvmsss2  35286  satfvsuclem2  35372  satfrel  35379  satfrnmapom  35382  satfv0fun  35383  satf00  35386  satf0suclem  35387  fmlasuc0  35396  msubrn  35541  dfon2lem7  35802  brbigcup  35911  elsingles  35931  fnimage  35942  funpartlem  35955  dfrdg4  35964  imagesset  35966  altopthsn  35974  elaltxp  35988  ellines  36165  linethru  36166  rankeq1o  36184  elhf2  36188  hfninf  36199  nn0prpwlem  36335  fneref  36363  neibastop2lem  36373  limsucncmpi  36458  bj-exlimmpbir  36927  curryset  36959  bj-snglex  36986  bj-restpw  37105  bj-inftyexpidisj  37223  topdifinffinlem  37360  relowlssretop  37376  rdgeqoa  37383  finxpreclem6  37409  fvineqsneq  37425  pibt2  37430  poimirlem23  37662  poimirlem29  37668  poimirlem31  37670  volsupnfl  37684  cnambfre  37687  dvasin  37723  dvacos  37724  sdclem2  37761  sstotbnd2  37793  ssbnd  37807  ismgmOLD  37869  grpokerinj  37912  rngomndo  37954  isdrngo1  37975  ac6s6  38191  iss2  38351  cnvelrels  38511  cosselrels  38512  brssrid  38518  brcnvssrid  38523  dfdisjs5  38729  eldisjs5  38743  mpets2  38858  pets  38869  prtlem12  38885  riotasv2d  38975  lkrscss  39116  islshpkrN  39138  isline  39757  ispointN  39760  0psubN  39767  linepsubN  39770  atpsubN  39771  cdlemk36  40931  diafn  41052  dibfna  41172  dibvalrel  41181  dicvalrelN  41203  diclspsn  41212  dihvalrel  41297  dih1  41304  lclkrlem1  41524  lclkr  41551  mapd1o  41666  mapdin  41680  hdmapfnN  41847  hgmapfnN  41906  lcmineqlem10  42050  sticksstones9  42166  sn-iotalem  42233  readvrec2  42373  readvrec  42374  repncan2  42394  elrfirn  42707  ismrcd1  42710  istopclsd  42712  rabren3dioph  42827  jm2.17b  42973  jm2.22  43007  jm2.23  43008  ttac  43048  pw2f1ocnv  43049  dnnumch1  43056  hbtlem5  43140  mncn0  43151  aaitgo  43174  rngunsnply  43181  unielss  43230  onexlimgt  43255  cantnfresb  43336  dflim5  43341  naddwordnexlem4  43413  safesnsupfiss  43427  safesnsupfidom1o  43429  safesnsupfilb  43430  ensucne0OLD  43542  clcnvlem  43635  relexp01min  43725  ntrf  44135  ssrecnpr  44320  seff  44321  sblpnf  44322  nzss  44329  dvconstbi  44346  ipo0  44460  ifr0  44461  addrfn  44483  subrfn  44484  mulvfn  44485  wfaxrep  45006  refsum2cnlem1  45053  rn1st  45289  ellimciota  45633  dvmptconst  45932  dvmptidg  45934  dvmulcncf  45942  dvdivcncf  45944  stoweidlem26  46043  stoweidlem50  46067  stoweidlem57  46074  aiotaval  47105  ndfatafv2nrn  47231  afv2ndefb  47234  funop1  47293  fun2dmnopgexmpl  47294  2ffzoeq  47337  2ltceilhalf  47338  m1modne  47358  iccpartiltu  47432  iccpartigtl  47433  zofldiv2ALTV  47672  evenprm2  47724  9fppr8  47747  stgoldbwt  47786  nnsum3primesle9  47804  nnsum4primeseven  47810  nnsum4primesevenALTV  47811  tgblthelfgott  47825  dfclnbgr6  47866  cycl3grtri  47957  grtrimap  47958  stgredgel  47967  stgr1  47971  isubgr3stgrlem2  47977  isubgr3stgrlem3  47978  usgrexmpl2trifr  48047  gpg5nbgrvtx13starlem1  48081  gpg5nbgrvtx13starlem2  48082  gpg5nbgrvtx13starlem3  48083  gpg5nbgr3star  48091  gpg3kgrtriex  48099  uspgrex  48160  0mgm  48176  nnsgrpmgm  48186  rngchomffvalALTV  48288  rhmsubcALTVlem1  48291  funcringcsetcALTV2lem4  48303  funcringcsetclem4ALTV  48326  srhmsubcALTV  48335  mapsnop  48354  zlmodzxzldeplem4  48514  zofldiv2  48542  fdivval  48550  nnlog2ge0lt1  48577  dig1  48619  itcoval2  48675  itcoval3  48676  mosn  48823  mo0  48824  mof02  48849  mofeu  48858  f102g  48862  f1mo  48863  tposres0  48887  f1omo  48903  f1omoOLD  48904  resipos  48985  intubeu  48994  unilbeu  48995  sectfn  49040  nelsubclem  49078  idfu1stf1o  49110  imaidfu  49121  oppfvallem  49146  funcoppc3  49158  idfth  49169  idsubc  49171  uptposlem  49208  swapf2fn  49279  swapf1f1o  49286  swapf2f1o  49287  swapf2f1oaALT  49289  fucof1  49333  fucofn2  49335  fucofn22  49351  reldmprcof1  49392  reldmprcof2  49393  fucoppcid  49419  fucoppc  49421  functhinclem1  49455  fullthinc  49461  thincciso  49464  indcthing  49471  indthinc  49473  indthincALT  49474  functermc  49519  discsntermlem  49581  reldmlan2  49628  reldmran2  49629  rellan  49634  relran  49635  termolmd  49681