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  7082  funop  7096  funsndifnop  7098  fnsnbOLD  7114  eufnfv  7177  f1ounsn  7220  f1eqcocnv  7249  nfriotadw  7325  nfriotad  7328  riotaprop  7344  oprabidw  7391  oprabid  7392  elrnmpo  7496  ov6g  7524  ovelrn  7536  caovmo  7597  offn  7637  caofinvl  7656  fr3nr  7719  onprc  7725  ordeleqon  7729  onint0  7738  0elsuc  7779  onuninsuci  7784  orduninsuc  7787  ordzsl  7789  onzsl  7790  tfinds  7804  limomss  7815  limom  7826  peano5  7837  xpexr  7862  eqop2  7978  opreuopreu  7980  1stconst  8044  2ndconst  8045  frxp2  8088  frxp3  8095  funsssuppss  8134  dftpos3  8188  dftpos4  8189  oawordeulem  8483  omwordi  8500  nnmwordi  8565  riiner  8731  ecopover  8762  map0g  8826  mapsnd  8828  elixpsn  8879  en0  8959  en0ALT  8960  en0r  8961  en1  8965  snfi  8984  fiprc  8985  sbthlem2  9020  sbthlem4  9022  sbthlem5  9023  0domg  9036  findcard  9092  findcard2  9093  nneneq  9134  sdom1  9154  1sdom2dom  9158  fineqvlem  9170  nfielex  9178  enp1i  9183  elfiun  9337  marypha1lem  9340  oicl  9438  oif  9439  oion  9445  hartogslem1  9451  hartogs  9453  wemapso2  9462  card2on  9463  0wdom  9479  brwdom2  9482  inf3lem6  9546  cantnflem3  9604  cantnflem4  9605  wemapwe  9610  cnfcom  9613  ssttrcl  9628  ttrclselem2  9639  tctr  9651  r1tr  9692  r1rankidb  9720  r1pw  9761  scottex  9801  scott0  9802  bnd2  9809  eldju2ndl  9840  tskwe  9866  oncard  9876  cardlim  9888  harsdom  9911  en2eleq  9922  dfac8alem  9943  cardaleph  10003  iunfictbso  10028  infmap2  10131  ackbij1lem18  10150  cff  10162  cfsuc  10171  cff1  10172  cflim2  10177  cfss  10179  sdom2en01  10216  infpssrlem4  10220  fin23lem7  10230  fin23lem11  10231  isfin2-2  10233  fin23lem26  10239  fin23lem19  10250  fin23lem17  10252  isf34lem2  10287  isf34lem4  10291  fin1a2lem6  10319  fin1a2lem10  10323  fin1a2lem12  10325  itunifn  10331  hsmexlem1  10340  axcc2lem  10350  dcomex  10361  axdc3lem4  10367  ondomon  10477  konigthlem  10483  pwcfsdom  10498  cfpwsdom  10499  axpowndlem3  10514  canth4  10562  canthnumlem  10563  canthwelem  10565  canthwe  10566  canthp1lem2  10568  pwfseqlem4  10577  pwfseqlem5  10578  gchaleph  10586  gch2  10590  winainflem  10608  0tsk  10670  rankcf  10692  tskcard  10696  gruina  10733  grutsk  10737  tskmid  10755  indpi  10822  nqereu  10844  mulcanenq  10875  recmulnq  10879  archnq  10895  ltsopr  10947  1ne0sr  11011  0idsr  11012  00sr  11014  leid  11233  lelttric  11244  divcan3  11826  divid  11831  div0  11833  lemul1a  11999  nn1suc  12171  nn0n0n1ge2b  12474  xnn0xr  12483  xnn0nemnf  12489  nn0lt10b  12558  nn0ind-raph  12596  elnn1uz2  12842  indstr2  12844  uzsupss  12857  rpnnen1lem4  12897  rpnnen1lem5  12898  xrnemnf  13035  xrnepnf  13036  mnfltxr  13045  xnn0n0n1ge2b  13050  xnn0ge0  13052  xrlttri  13057  xrlttr  13058  xrleid  13069  qbtwnxr  13119  xmullem2  13184  xlemul1a  13207  xrub  13231  reltxrnmnf  13262  ixxun  13281  xnn0xrge0  13426  fztpval  13506  fseq1p1m1  13518  elfznelfzob  13694  ltweuz  13888  fzfi  13899  fsuppmapnn0fiubex  13919  ser0f  13982  0exp  14024  faclbnd4lem1  14220  bcn1  14240  hashnemnf  14271  hashv01gt1  14272  hashsnle1  14344  hashgt12el2  14350  hashpw  14363  hashf1  14384  fz1isolem  14388  hash2prb  14399  hash3tpb  14422  0wrd0  14467  wrdlen1  14481  ccatvalfn  14508  eqs1  14540  wrdl1exs1  14541  swrdlen  14575  swrdwrdsymb  14590  swrdspsleq  14593  cats1un  14648  wrdind  14649  wrd2ind  14650  swrdccatin1  14652  repswsymballbi  14707  cshw1  14749  scshwfzeqfzo  14753  wrdl2exs2  14873  trclfvcotr  14936  relexp1g  14953  relexp0rel  14964  relexprelg  14965  relexpreld  14967  sqrt0  15168  sqrtsq  15196  mptfzshft  15705  prodf1f  15819  egt2lt3  16135  0dvds  16207  nn0onn  16311  nn0o  16314  divalgmod  16337  flodddiv4  16346  bitsp1o  16364  gcddvds  16434  bezout  16474  lcmdvds  16539  rpdvds  16591  1nprm  16610  prmind2  16616  dvdszzq  16652  nnoddn2prmb  16745  pcpre1  16774  vdwapf  16904  vdwapid1  16907  ram0  16954  ramz  16957  prmolefac  16978  cshws0  17033  prmlem0  17037  strle1  17089  restsspw  17355  prdsdsfn  17389  imasdsfn  17439  imasaddfnlem  17453  imasvscafn  17462  xpsfrnel  17487  isacs1i  17584  cidfn  17606  fnhomeqhomf  17618  comffn  17632  isoval  17693  sscres  17751  cofucl  17816  idffth  17863  ressffth  17868  cat1lem  18024  catcoppccl  18045  estrchomfn  18062  funcestrcsetclem4  18070  funcestrcsetclem7  18073  equivestrcsetc  18079  funcsetcestrclem4  18085  funcsetcestrclem7  18088  1stfcl  18124  2ndfcl  18125  prfcl  18130  evlfcl  18149  curf1cl  18155  curfcl  18159  hofcl  18186  yonedainv  18208  pospo  18270  lubfun  18277  glbfun  18290  joindmss  18304  meetdmss  18318  ipopos  18463  acsficl2d  18479  dirref  18528  mgmidcl  18595  mgmlrid  18596  ielefmnd  18816  smndex1basss  18834  smndex1n0mnd  18841  cntzssv  19261  idresperm  19319  symgvalstruct  19330  pmtrfmvdn0  19395  symggen  19403  psgnunilem1  19426  psgnprfval  19454  slwpgp  19546  frgpmhm  19698  frgpuptinv  19704  frgpup3lem  19710  gsumzoppg  19877  gsumcom2  19908  c0snmhm  20403  srhmsubc  20617  rhmsubclem1  20622  rrgsupp  20638  abv0  20760  zrhrhm  21470  psgnodpmr  21549  frlmphllem  21739  ellspd  21761  psrvscafval  21908  psrridm  21922  ltbwe  22003  psrbag0  22021  psrbagsn  22022  subrgascl  22025  psdmul  22113  mattpostpos  22402  mavmul0  22500  mavmul0g  22501  mdet0f1o  22541  m1detdiag  22545  m2detleiblem5  22573  m2detleiblem6  22574  m2detleiblem3  22577  m2detleiblem4  22578  maducoeval2  22588  d1mat2pmat  22687  chpmat1dlem  22783  chpmat1d  22784  baspartn  22902  eltg3  22910  topnex  22944  fctop  22952  cctop  22954  discld  23037  mretopd  23040  neipeltop  23077  neitr  23128  restcls  23129  ordtbaslem  23136  ordtuni  23138  idcn  23205  cnrmi  23308  cmpsublem  23347  cmpsub  23348  tgcmp  23349  uncmp  23351  hauscmplem  23354  cmpfi  23356  bwth  23358  1stcrestlem  23400  disllycmp  23446  dis1stc  23447  refref  23461  kgeni  23485  1stckgenlem  23501  kqffn  23673  snfil  23812  filconn  23831  cfinfil  23841  ufileu  23867  filufint  23868  fixufil  23870  cfinufil  23876  ufilen  23878  fin1aufil  23880  fmf  23893  rnelfm  23901  flimclslem  23932  hauspwpwf1  23935  supnfcls  23968  flimfnfcls  23976  fclscmp  23978  alexsubALTlem2  23996  alexsubALTlem3  23997  alexsubALT  23999  ptcmplem1  24000  cnextrel  24011  tsmsfbas  24076  ustref  24167  trust  24177  restutop  24185  isusp  24209  xmet0  24290  imasdsf1olem  24321  blfvalps  24331  blfps  24354  blf  24355  restmetu  24518  dscmet  24520  isngp2  24545  nm0  24577  nrginvrcn  24640  nmoix  24677  qdensere  24717  iccconn  24779  iccpnfcnv  24902  xrhmeo  24904  lebnumlem3  24922  metsscmetcld  25275  bcthlem5  25288  csschl  25336  rrxmfval  25366  minveclem3b  25388  cniccbdd  25422  ovolicc2lem4  25481  iunmbl  25514  ioorinv  25537  ioorcl  25538  i1f1lem  25650  limcvallem  25832  ellimc2  25838  limccnp  25852  limccnp2  25853  limcco  25854  perfdvf  25864  recnprss  25865  fncpn  25895  dvcmulf  25908  c1lip1  25962  lhop2  25980  q1pcl  26122  r1pdeglt  26125  ply1remlem  26130  plyssc  26165  ulm0  26360  cxpeq0  26647  cxplea  26665  cxplogb  26756  asinlem  26838  isppw2  27085  muval2  27104  dchrfi  27226  dchrpt  27238  bposlem6  27260  lgsdir2lem2  27297  lgsqr  27322  gausslemma2dlem4  27340  2lgslem2  27366  2lgslem3  27375  2lgs  27378  2sqlem7  27395  2sqlem11  27400  chtppilim  27446  nosgnn0i  27631  nolesgn2ores  27644  nogesgn1ores  27646  nosepnelem  27651  nosepdmlem  27655  nosupbnd1lem3  27682  nosupbnd1lem5  27684  nosupbnd2lem1  27687  noinfbnd1lem3  27697  noinfbnd1lem5  27699  noinfbnd2lem1  27702  oldval  27832  made0  27855  lrrecpo  27923  pncan2s  28056  divscan3d  28217  abssor  28227  om2noseqfo  28279  noseqrdglem  28286  noseqrdgfn  28287  noseqrdg0  28288  onsfi  28336  nohalf  28403  expsne0  28415  pw2divscan3d  28420  tgldimor  28557  tgcgr4  28586  tglnfn  28602  tglnunirn  28603  mirne  28722  mircinv  28723  perpln1  28765  perpln2  28766  lmiisolem  28851  xmstrkgc  28941  axcgrtr  28971  axsegconlem9  28981  axlowdimlem5  29002  axlowdimlem17  29014  axlowdim1  29015  uhgr0e  29127  edglnl  29199  uhgr0edgfi  29296  issubgr2  29328  subgrprop2  29330  egrsubgr  29333  0grsubgr  29334  0uhgrsubgr  29335  uhgrsubgrself  29336  nbgr1vtx  29414  nbgrssovtx  29417  nb3grprlem1  29436  uvtx01vtx  29453  cplgr1vlem  29485  cplgr1v  29486  usgrexilem  29496  wlkcomp  29687  wlk1walk  29695  wlkp1lem5  29732  uhgrwkspthlem1  29809  pthdlem1  29822  clwlkcomp  29835  lfgrn1cycl  29861  uspgrn2crct  29864  wwlksn0s  29917  usgrwwlks2on  30014  umgrwwlks2on  30015  clwwlkn  30084  clwwlkn1  30099  0ewlk  30172  1ewlk  30173  0spth  30184  upgr1wlkdlem2  30204  wlk2v2e  30215  upgr3v3e3cycl  30238  upgr4cycl4dv4e  30243  eupth0  30272  frgr0v  30320  frgr1v  30329  1vwmgr  30334  ex-opab  30490  grpoinvf  30590  nvmid  30717  nmlnoubi  30854  hiidrcl  31153  hsn0elch  31306  shjshseli  31551  cmbr4i  31659  dfiop2  31811  kbpj  32014  nmopun  32072  adjeq0  32149  kbass2  32175  pjssdif1i  32233  pjinvari  32249  pjcmul2i  32260  pj3i  32266  stge1i  32296  stle0i  32297  sumdmdlem2  32477  dmdbr6ati  32481  dmdbr7ati  32482  rabsnel  32557  unidifsnel  32592  unidifsnne  32593  disjdifprg  32632  ofoprabco  32724  padct  32778  fpwrelmapffslem  32792  nn0mnfxrd  32812  xrlelttric  32813  xnn0gt0  32830  iundisj2cnt  32860  f1ocnt  32861  fz1nnct  32862  fz1nntr  32863  hashxpe  32868  nn0min  32882  sgnmulsgn  32904  sgnmulsgp  32905  wrdt2ind  33016  xrge0tsmsbi  33137  opprabs  33544  rtelextdg2lem  33864  2sqr3minply  33918  locfinref  33979  dispcmp  33997  zartopn  34013  zarcmplem  34019  pstmxmet  34035  xrge0iifcnv  34071  xrge0iif1  34076  qqhre  34158  esumcl  34168  esumpr2  34205  esumpinfval  34211  esumpcvgval  34216  ofcfn  34238  pwsiga  34268  prsiga  34269  sigainb  34274  ldgenpisyslem1  34301  measiuns  34355  relfae  34385  pmeasmono  34462  sitgf  34485  eulerpartgbij  34510  signswch  34699  signslema  34700  signstlen  34705  signstfvn  34707  circlevma  34780  bnj216  34869  bnj151  35014  bnj517  35022  bnj970  35084  bnj1145  35130  bnj1498  35198  r1omhfb  35249  fineqvrep  35251  fineqvac  35253  fineqvnttrclselem1  35258  fineqvnttrclselem2  35259  fineqvnttrclse  35261  fineqvinfep  35262  r1omhfbregs  35274  wevgblacfn  35284  0nn0m1nnn0  35288  pthhashvtx  35303  acycgr0v  35323  prclisacycgr  35326  umgracycusgr  35329  cusgracyclt3v  35331  subfacp1lem5  35359  erdszelem8  35373  kur14lem1  35381  indispconn  35409  cvmsss2  35449  satfvsuclem2  35535  satfrel  35542  satfrnmapom  35545  satfv0fun  35546  satf00  35549  satf0suclem  35550  fmlasuc0  35559  msubrn  35704  dfon2lem7  35962  brbigcup  36071  elsingles  36091  fnimage  36102  funpartlem  36117  dfrdg4  36126  imagesset  36128  altopthsn  36136  elaltxp  36150  ellines  36327  linethru  36328  rankeq1o  36346  elhf2  36350  hfninf  36361  nn0prpwlem  36497  fneref  36525  neibastop2lem  36535  limsucncmpi  36620  bj-exlimmpbir  37090  curryset  37122  bj-snglex  37149  bj-restpw  37268  bj-inftyexpidisj  37386  topdifinffinlem  37523  relowlssretop  37539  rdgeqoa  37546  finxpreclem6  37572  fvineqsneq  37588  pibt2  37593  poimirlem23  37815  poimirlem29  37821  poimirlem31  37823  volsupnfl  37837  cnambfre  37840  dvasin  37876  dvacos  37877  sdclem2  37914  sstotbnd2  37946  ssbnd  37960  ismgmOLD  38022  grpokerinj  38065  rngomndo  38107  isdrngo1  38128  ac6s6  38344  iss2  38516  relecxrn  38579  sucmapsuc  38661  cosselrels  38747  cnvelrels  38748  brssrid  38754  brcnvssrid  38759  dfdisjs5  38969  eldisjs5  38995  eldisjsim3  39109  mpets2  39127  pets  39138  prtlem12  39164  riotasv2d  39254  lkrscss  39395  islshpkrN  39417  isline  40036  ispointN  40039  0psubN  40046  linepsubN  40049  atpsubN  40050  cdlemk36  41210  diafn  41331  dibfna  41451  dibvalrel  41460  dicvalrelN  41482  diclspsn  41491  dihvalrel  41576  dih1  41583  lclkrlem1  41803  lclkr  41830  mapd1o  41945  mapdin  41959  hdmapfnN  42126  hgmapfnN  42185  lcmineqlem10  42329  sticksstones9  42445  sn-iotalem  42514  readvrec2  42652  readvrec  42653  repncan2  42673  elrfirn  42973  ismrcd1  42976  istopclsd  42978  rabren3dioph  43093  jm2.17b  43239  jm2.22  43273  jm2.23  43274  ttac  43314  pw2f1ocnv  43315  dnnumch1  43322  hbtlem5  43406  mncn0  43417  aaitgo  43440  rngunsnply  43447  unielss  43496  onexlimgt  43521  cantnfresb  43602  dflim5  43607  naddwordnexlem4  43679  safesnsupfiss  43692  safesnsupfidom1o  43694  safesnsupfilb  43695  ensucne0OLD  43807  clcnvlem  43900  relexp01min  43990  ntrf  44400  ssrecnpr  44585  seff  44586  sblpnf  44587  nzss  44594  dvconstbi  44611  ipo0  44725  ifr0  44726  addrfn  44748  subrfn  44749  mulvfn  44750  wfaxrep  45271  refsum2cnlem1  45318  rn1st  45553  ellimciota  45896  dvmptconst  46195  dvmptidg  46197  dvmulcncf  46205  dvdivcncf  46207  stoweidlem26  46306  stoweidlem50  46330  stoweidlem57  46337  aiotaval  47377  ndfatafv2nrn  47503  afv2ndefb  47506  funop1  47565  fun2dmnopgexmpl  47566  2ffzoeq  47609  2ltceilhalf  47610  m1modne  47630  iccpartiltu  47704  iccpartigtl  47705  zofldiv2ALTV  47944  evenprm2  47996  9fppr8  48019  stgoldbwt  48058  nnsum3primesle9  48076  nnsum4primeseven  48082  nnsum4primesevenALTV  48083  tgblthelfgott  48097  dfclnbgr6  48138  cycl3grtri  48229  grtrimap  48230  stgredgel  48239  stgr1  48243  isubgr3stgrlem2  48249  isubgr3stgrlem3  48250  usgrexmpl2trifr  48319  gpg5nbgrvtx13starlem1  48353  gpg5nbgrvtx13starlem2  48354  gpg5nbgrvtx13starlem3  48355  gpg5nbgr3star  48363  gpg3kgrtriex  48371  uspgrex  48432  0mgm  48448  nnsgrpmgm  48458  rngchomffvalALTV  48560  rhmsubcALTVlem1  48563  funcringcsetcALTV2lem4  48575  funcringcsetclem4ALTV  48598  srhmsubcALTV  48607  mapsnop  48626  zlmodzxzldeplem4  48785  zofldiv2  48813  fdivval  48821  nnlog2ge0lt1  48848  dig1  48890  itcoval2  48946  itcoval3  48947  mosn  49094  mo0  49095  mof02  49120  mofeu  49129  f102g  49133  f1mo  49134  tposres0  49158  f1omo  49174  f1omoOLD  49175  resipos  49256  intubeu  49265  unilbeu  49266  sectfn  49310  nelsubclem  49348  idfu1stf1o  49380  imaidfu  49391  oppfvallem  49416  funcoppc3  49428  idfth  49439  idsubc  49441  uptposlem  49478  swapf2fn  49549  swapf1f1o  49556  swapf2f1o  49557  swapf2f1oaALT  49559  fucof1  49603  fucofn2  49605  fucofn22  49621  reldmprcof1  49662  reldmprcof2  49663  fucoppcid  49689  fucoppc  49691  functhinclem1  49725  fullthinc  49731  thincciso  49734  indcthing  49741  indthinc  49743  indthincALT  49744  functermc  49789  discsntermlem  49851  reldmlan2  49898  reldmran2  49899  rellan  49904  relran  49905  termolmd  49951