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 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  1084  spei  2394  nfald2  2445  nfabd2  2930  raleleqALT  3342  dedhb  3700  sbceqalOLD  3845  csbie2df  4441  ssdifeq0  4487  r19.2zb  4496  dedth  4587  pwidg  4623  elpr2OLD  4655  snidg  4663  rexreusng  4684  exsnrex  4685  ifpr  4696  rmosn  4724  rabrsn  4729  prid1g  4765  tpid1g  4774  tpid2g  4776  tpid3g  4777  pwpw0  4817  sssn  4830  elpreqpr  4868  pwsnOLD  4902  unimax  4949  intmin3  4981  eqbrtrdi  5188  al0ssb  5309  intabs  5343  pwnss  5350  difelpw  5352  rabelpw  5353  0inp0  5358  intidg  5458  copsexgw  5491  copsexg  5492  euotd  5514  elopab  5528  elvvuni  5753  posn  5762  frsn  5764  eqrelriv  5790  relsnb  5803  relopabiALT  5824  opabid2  5829  ididg  5854  iss  6036  dfpo2  6296  ord0eln0  6420  sucidg  6446  nsuceq0  6448  funopg  6583  fn0  6682  f00  6774  f0bi  6775  f10d  6868  f1o00  6869  fo00  6870  brprcneu  6882  brprcneuALT  6883  dffn5  6951  fsn  7133  funop  7147  funsndifnop  7149  fnsnb  7164  eufnfv  7231  f1eqcocnv  7299  f1eqcocnvOLD  7300  nfriotadw  7373  nfriotad  7377  riotaprop  7393  oprabidw  7440  oprabid  7441  elrnmpo  7545  ov6g  7571  ovelrn  7583  caovmo  7644  offn  7683  caofinvl  7700  fr3nr  7759  onprc  7765  ordeleqon  7769  onint0  7779  0elsuc  7823  onuninsuci  7829  orduninsuc  7832  ordzsl  7834  onzsl  7835  tfinds  7849  limomss  7860  limom  7871  peano5  7884  peano5OLD  7885  xpexr  7909  eqop2  8018  opreuopreu  8020  1stconst  8086  2ndconst  8087  frxp2  8130  frxp3  8137  funsssuppss  8175  dftpos3  8229  dftpos4  8230  wfrlem4OLD  8312  wfrlem14OLD  8322  oawordeulem  8554  omwordi  8571  nnmwordi  8635  riiner  8784  ecopover  8815  map0g  8878  mapsnd  8880  elixpsn  8931  en0  9013  en0OLD  9014  en0ALT  9015  en0r  9016  en1  9021  en1OLD  9022  fiprc  9045  sbthlem2  9084  sbthlem4  9086  sbthlem5  9087  0domg  9100  findcard  9163  findcard2  9164  nneneq  9209  nneneqOLD  9221  sdom1  9242  sdom1OLD  9243  1sdom2dom  9247  fineqvlem  9262  nfielex  9273  enp1i  9279  findcard2OLD  9284  elfiun  9425  marypha1lem  9428  oicl  9524  oif  9525  oion  9531  hartogslem1  9537  hartogs  9539  wemapso2  9548  card2on  9549  0wdom  9565  brwdom2  9568  inf3lem6  9628  cantnflem3  9686  cantnflem4  9687  wemapwe  9692  cnfcom  9695  ssttrcl  9710  ttrclselem2  9721  tctr  9735  r1tr  9771  r1rankidb  9799  r1pw  9840  scottex  9880  scott0  9881  bnd2  9888  eldju2ndl  9919  tskwe  9945  oncard  9955  cardlim  9967  harsdom  9990  en2eleq  10003  dfac8alem  10024  cardaleph  10084  iunfictbso  10109  infmap2  10213  ackbij1lem18  10232  cff  10243  cfsuc  10252  cff1  10253  cflim2  10258  cfss  10260  sdom2en01  10297  infpssrlem4  10301  fin23lem7  10311  fin23lem11  10312  isfin2-2  10314  fin23lem26  10320  fin23lem19  10331  fin23lem17  10333  isf34lem2  10368  isf34lem4  10372  fin1a2lem6  10400  fin1a2lem10  10404  fin1a2lem12  10406  itunifn  10412  hsmexlem1  10421  axcc2lem  10431  dcomex  10442  axdc3lem4  10448  ondomon  10558  konigthlem  10563  pwcfsdom  10578  cfpwsdom  10579  axpowndlem3  10594  canth4  10642  canthnumlem  10643  canthwelem  10645  canthwe  10646  canthp1lem2  10648  pwfseqlem4  10657  pwfseqlem5  10658  gchaleph  10666  gch2  10670  winainflem  10688  0tsk  10750  rankcf  10772  tskcard  10776  gruina  10813  grutsk  10817  tskmid  10835  indpi  10902  nqereu  10924  mulcanenq  10955  recmulnq  10959  archnq  10975  ltsopr  11027  1ne0sr  11091  0idsr  11092  00sr  11094  leid  11310  lelttric  11321  divcan3  11898  lemul1a  12068  nn1suc  12234  nn0n0n1ge2b  12540  xnn0xr  12549  xnn0nemnf  12555  nn0lt10b  12624  nn0ind-raph  12662  elnn1uz2  12909  indstr2  12911  uzsupss  12924  rpnnen1lem4  12964  rpnnen1lem5  12965  xrnemnf  13097  xrnepnf  13098  mnfltxr  13107  xnn0n0n1ge2b  13111  xnn0ge0  13113  xrlttri  13118  xrlttr  13119  xrleid  13130  qbtwnxr  13179  xmullem2  13244  xlemul1a  13267  xrub  13291  reltxrnmnf  13321  ixxun  13340  xnn0xrge0  13483  fztpval  13563  fseq1p1m1  13575  elfznelfzob  13738  ltweuz  13926  fzfi  13937  fsuppmapnn0fiubex  13957  ser0f  14021  0exp  14063  faclbnd4lem1  14253  bcn1  14273  hashnemnf  14304  hashv01gt1  14305  hashsnle1  14377  hashgt12el2  14383  hashpw  14396  hashf1  14418  fz1isolem  14422  hash2prb  14433  0wrd0  14490  wrdlen1  14504  ccatvalfn  14531  eqs1  14562  wrdl1exs1  14563  swrdlen  14597  swrdwrdsymb  14612  swrdspsleq  14615  cats1un  14671  wrdind  14672  wrd2ind  14673  swrdccatin1  14675  repswsymballbi  14730  cshw1  14772  scshwfzeqfzo  14777  wrdl2exs2  14897  trclfvcotr  14956  relexp1g  14973  relexp0rel  14984  relexprelg  14985  relexpreld  14987  sqrt0  15188  sqrtsq  15216  mptfzshft  15724  prodf1f  15838  egt2lt3  16149  0dvds  16220  nn0onn  16323  nn0o  16326  divalgmod  16349  flodddiv4  16356  bitsp1o  16374  gcddvds  16444  bezout  16485  lcmdvds  16545  rpdvds  16597  1nprm  16616  prmind2  16622  nnoddn2prmb  16746  pcpre1  16775  vdwapf  16905  vdwapid1  16908  ram0  16955  ramz  16958  prmolefac  16979  cshws0  17035  prmlem0  17039  strle1  17091  restsspw  17377  prdsdsfn  17411  imasdsfn  17460  imasaddfnlem  17474  imasvscafn  17483  xpsfrnel  17508  isacs1i  17601  cidfn  17623  fnhomeqhomf  17635  comffn  17649  isoval  17712  sscres  17770  cofucl  17838  idffth  17884  ressffth  17889  cat1lem  18046  catcoppccl  18067  catcoppcclOLD  18068  estrchomfn  18086  funcestrcsetclem4  18095  funcestrcsetclem7  18098  equivestrcsetc  18104  funcsetcestrclem4  18110  funcsetcestrclem7  18113  1stfcl  18149  2ndfcl  18150  prfcl  18155  evlfcl  18175  curf1cl  18181  curfcl  18185  hofcl  18212  yonedainv  18234  pospo  18298  lubfun  18305  glbfun  18318  joindmss  18332  meetdmss  18346  ipopos  18489  acsficl2d  18505  dirref  18554  mgmidcl  18585  mgmlrid  18586  ielefmnd  18768  smndex1basss  18786  smndex1n0mnd  18793  cntzssv  19192  idresperm  19253  symgvalstruct  19264  symgvalstructOLD  19265  pmtrfmvdn0  19330  symggen  19338  psgnunilem1  19361  psgnprfval  19389  slwpgp  19481  frgpmhm  19633  frgpuptinv  19639  frgpup3lem  19645  gsumzoppg  19812  gsumcom2  19843  abv0  20439  rrgsupp  20907  zrhrhm  21061  psgnodpmr  21143  frlmphllem  21335  ellspd  21357  psrvscafval  21509  psrridm  21524  ltbwe  21599  psrbag0  21623  psrbagsn  21624  subrgascl  21627  mattpostpos  21956  mavmul0  22054  mavmul0g  22055  mdet0f1o  22095  m1detdiag  22099  m2detleiblem5  22127  m2detleiblem6  22128  m2detleiblem3  22131  m2detleiblem4  22132  maducoeval2  22142  d1mat2pmat  22241  chpmat1dlem  22337  chpmat1d  22338  baspartn  22457  eltg3  22465  topnex  22499  fctop  22507  cctop  22509  discld  22593  mretopd  22596  neipeltop  22633  neitr  22684  restcls  22685  ordtbaslem  22692  ordtuni  22694  idcn  22761  cnrmi  22864  cmpsublem  22903  cmpsub  22904  tgcmp  22905  uncmp  22907  hauscmplem  22910  cmpfi  22912  bwth  22914  1stcrestlem  22956  disllycmp  23002  dis1stc  23003  refref  23017  kgeni  23041  1stckgenlem  23057  kqffn  23229  snfil  23368  filconn  23387  cfinfil  23397  ufileu  23423  filufint  23424  fixufil  23426  cfinufil  23432  ufilen  23434  fin1aufil  23436  fmf  23449  rnelfm  23457  flimclslem  23488  hauspwpwf1  23491  supnfcls  23524  flimfnfcls  23532  fclscmp  23534  alexsubALTlem2  23552  alexsubALTlem3  23553  alexsubALT  23555  ptcmplem1  23556  cnextrel  23567  tsmsfbas  23632  ustref  23723  trust  23734  restutop  23742  isusp  23766  xmet0  23848  imasdsf1olem  23879  blfvalps  23889  blfps  23912  blf  23913  restmetu  24079  dscmet  24081  isngp2  24106  nm0  24138  nrginvrcn  24209  nmoix  24246  qdensere  24286  iccconn  24346  iccpnfcnv  24460  xrhmeo  24462  lebnumlem3  24479  metsscmetcld  24832  bcthlem5  24845  csschl  24893  rrxmfval  24923  minveclem3b  24945  cniccbdd  24978  ovolicc2lem4  25037  iunmbl  25070  ioorinv  25093  ioorcl  25094  i1f1lem  25206  limcvallem  25388  ellimc2  25394  limccnp  25408  limccnp2  25409  limcco  25410  perfdvf  25420  recnprss  25421  fncpn  25450  dvcmulf  25462  c1lip1  25514  lhop2  25532  q1pcl  25673  r1pdeglt  25676  ply1remlem  25680  plyssc  25714  ulm0  25903  cxpeq0  26186  cxplea  26204  cxplogb  26291  asinlem  26373  isppw2  26619  muval2  26638  dchrfi  26758  dchrpt  26770  bposlem6  26792  lgsdir2lem2  26829  lgsqr  26854  gausslemma2dlem4  26872  2lgslem2  26898  2lgslem3  26907  2lgs  26910  2sqlem7  26927  2sqlem11  26932  chtppilim  26978  nosgnn0i  27162  nolesgn2ores  27175  nogesgn1ores  27177  nosepnelem  27182  nosepdmlem  27186  nosupbnd1lem3  27213  nosupbnd1lem5  27215  nosupbnd2lem1  27218  noinfbnd1lem3  27228  noinfbnd1lem5  27230  noinfbnd2lem1  27233  oldval  27349  made0  27368  lrrecpo  27425  tgldimor  27753  tgcgr4  27782  tglnfn  27798  tglnunirn  27799  mirne  27918  mircinv  27919  perpln1  27961  perpln2  27962  lmiisolem  28047  xmstrkgc  28143  axcgrtr  28173  axsegconlem9  28183  axlowdimlem5  28204  axlowdimlem17  28216  axlowdim1  28217  uhgr0e  28331  edglnl  28403  uhgr0edgfi  28497  issubgr2  28529  subgrprop2  28531  egrsubgr  28534  0grsubgr  28535  0uhgrsubgr  28536  uhgrsubgrself  28537  nbgr0vtx  28613  nbgr1vtx  28615  nbgrssovtx  28618  nb3grprlem1  28637  uvtx01vtx  28654  cplgr1vlem  28686  cplgr1v  28687  usgrexilem  28697  wlkcomp  28888  wlk1walk  28896  wlkp1lem5  28934  uhgrwkspthlem1  29010  pthdlem1  29023  clwlkcomp  29036  lfgrn1cycl  29059  uspgrn2crct  29062  wwlksn0s  29115  umgrwwlks2on  29211  clwwlkn  29279  clwwlkn1  29294  0ewlk  29367  1ewlk  29368  0spth  29379  upgr1wlkdlem2  29399  wlk2v2e  29410  upgr3v3e3cycl  29433  upgr4cycl4dv4e  29438  eupth0  29467  frgr0v  29515  frgr1v  29524  1vwmgr  29529  ex-opab  29685  grpoinvf  29785  nvmid  29912  nmlnoubi  30049  hiidrcl  30348  hsn0elch  30501  shjshseli  30746  cmbr4i  30854  dfiop2  31006  kbpj  31209  nmopun  31267  adjeq0  31344  kbass2  31370  pjssdif1i  31428  pjinvari  31444  pjcmul2i  31455  pj3i  31461  stge1i  31491  stle0i  31492  sumdmdlem2  31672  dmdbr6ati  31676  dmdbr7ati  31677  rabsnel  31740  unidifsnel  31772  unidifsnne  31773  disjdifprg  31806  ofoprabco  31889  padct  31944  fpwrelmapffslem  31957  xrlelttric  31965  xnn0gt0  31982  iundisj2cnt  32010  f1ocnt  32013  fz1nnct  32014  fz1nntr  32015  hashxpe  32019  dvdszzq  32021  nn0min  32026  wrdt2ind  32117  xrge0tsmsbi  32210  opprabs  32596  locfinref  32821  dispcmp  32839  zartopn  32855  zarcmplem  32861  pstmxmet  32877  xrge0iifcnv  32913  xrge0iif1  32918  qqhre  33000  esumcl  33028  esumpr2  33065  esumpinfval  33071  esumpcvgval  33076  ofcfn  33098  pwsiga  33128  prsiga  33129  sigainb  33134  ldgenpisyslem1  33161  measiuns  33215  relfae  33245  pmeasmono  33323  sitgf  33346  eulerpartgbij  33371  sgnmulsgn  33548  sgnmulsgp  33549  signswch  33572  signslema  33573  signstlen  33578  signstfvn  33580  circlevma  33654  bnj216  33743  bnj151  33888  bnj517  33896  bnj970  33958  bnj1145  34004  bnj1498  34072  fineqvrep  34095  fineqvac  34097  0nn0m1nnn0  34102  pthhashvtx  34118  acycgr0v  34139  prclisacycgr  34142  umgracycusgr  34145  cusgracyclt3v  34147  subfacp1lem5  34175  erdszelem8  34189  kur14lem1  34197  indispconn  34225  cvmsss2  34265  satfvsuclem2  34351  satfrel  34358  satfrnmapom  34361  satfv0fun  34362  satf00  34365  satf0suclem  34366  fmlasuc0  34375  msubrn  34520  dfon2lem7  34761  brbigcup  34870  elsingles  34890  fnimage  34901  funpartlem  34914  dfrdg4  34923  imagesset  34925  altopthsn  34933  elaltxp  34947  ellines  35124  linethru  35125  rankeq1o  35143  elhf2  35147  hfninf  35158  nn0prpwlem  35207  fneref  35235  neibastop2lem  35245  limsucncmpi  35330  bj-exlimmpbir  35794  curryset  35827  bj-snglex  35854  bj-restpw  35973  bj-inftyexpidisj  36091  topdifinffinlem  36228  relowlssretop  36244  rdgeqoa  36251  finxpreclem6  36277  fvineqsneq  36293  pibt2  36298  poimirlem23  36511  poimirlem29  36517  poimirlem31  36519  volsupnfl  36533  cnambfre  36536  dvasin  36572  dvacos  36573  sdclem2  36610  sstotbnd2  36642  ssbnd  36656  ismgmOLD  36718  grpokerinj  36761  rngomndo  36803  isdrngo1  36824  ac6s6  37040  iss2  37213  cnvelrels  37365  cosselrels  37366  brssrid  37372  brcnvssrid  37377  dfdisjs5  37582  eldisjs5  37596  mpets2  37711  pets  37722  prtlem12  37737  riotasv2d  37827  lkrscss  37968  islshpkrN  37990  isline  38610  ispointN  38613  0psubN  38620  linepsubN  38623  atpsubN  38624  cdlemk36  39784  diafn  39905  dibfna  40025  dibvalrel  40034  dicvalrelN  40056  diclspsn  40065  dihvalrel  40150  dih1  40157  lclkrlem1  40377  lclkr  40404  mapd1o  40519  mapdin  40533  hdmapfnN  40700  hgmapfnN  40759  lcmineqlem10  40903  sticksstones9  40970  sn-iotalem  41038  repncan2  41255  sn-inelr  41338  elrfirn  41433  ismrcd1  41436  istopclsd  41438  rabren3dioph  41553  jm2.17b  41700  jm2.22  41734  jm2.23  41735  ttac  41775  pw2f1ocnv  41776  dnnumch1  41786  hbtlem5  41870  mncn0  41881  aaitgo  41904  rngunsnply  41915  unielss  41967  onexlimgt  41992  cantnfresb  42074  dflim5  42079  naddwordnexlem4  42152  safesnsupfiss  42166  safesnsupfidom1o  42168  safesnsupfilb  42169  ensucne0OLD  42281  clcnvlem  42374  relexp01min  42464  ntrf  42874  ssrecnpr  43067  seff  43068  sblpnf  43069  nzss  43076  dvconstbi  43093  ipo0  43208  ifr0  43209  addrfn  43231  subrfn  43232  mulvfn  43233  refsum2cnlem1  43721  rn1st  43978  ellimciota  44330  dvmptconst  44631  dvmptidg  44633  dvmulcncf  44641  dvdivcncf  44643  stoweidlem26  44742  stoweidlem50  44766  stoweidlem57  44773  aiotaval  45803  ndfatafv2nrn  45929  afv2ndefb  45932  funop1  45991  fun2dmnopgexmpl  45992  2ffzoeq  46036  iccpartiltu  46090  iccpartigtl  46091  zofldiv2ALTV  46330  evenprm2  46382  9fppr8  46405  stgoldbwt  46444  nnsum3primesle9  46462  nnsum4primeseven  46468  nnsum4primesevenALTV  46469  tgblthelfgott  46483  isomgreqve  46493  uspgrex  46528  0mgm  46544  nnsgrpmgm  46586  c0snmhm  46714  rngchomffvalALTV  46893  funcringcsetcALTV2lem4  46937  funcringcsetclem4ALTV  46960  srhmsubc  46974  rhmsubclem1  46984  srhmsubcALTV  46992  rhmsubcALTVlem1  47002  mapsnop  47020  zlmodzxzldeplem4  47184  zofldiv2  47217  fdivval  47225  nnlog2ge0lt1  47252  dig1  47294  itcoval2  47350  itcoval3  47351  mosn  47497  mo0  47498  mof02  47505  mofeu  47514  f102g  47518  f1mo  47519  f1omo  47527  intubeu  47609  unilbeu  47610  functhinclem1  47661  fullthinc  47666  thincciso  47669  indthinc  47672  indthincALT  47673