Theorem mpbiri 250

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 249	1 ⊢ (𝜑 → 𝜓)

Syntax hints:   → wi 4   ↔ wb 198

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 199

This theorem is referenced by:  elimh  1061  dedtOLD  1064  speiv  1931  spei  2325  nfald2  2381  nfabd2  2947  nfabd2OLD  2948  raleleqALT  3362  dedhb  3603  sbceqal  3732  ssdifeq0  4309  r19.2zb  4318  dedth  4400  pwidg  4431  elpr2  4459  snidg  4465  rexreusng  4485  exsnrex  4486  ifpr  4497  rmosn  4523  rabrsn  4528  prid1g  4564  tpid1g  4573  tpid2g  4575  tpid3g  4576  pwpw0  4614  sssn  4627  elpreqpr  4665  pwsnALT  4699  unimax  4741  intmin3  4771  syl6eqbr  4962  al0ssb  5063  intabs  5095  pwnss  5100  0inp0  5107  copsexg  5232  euotd  5253  elopab  5263  epelgOLD  5313  elvvuni  5472  posn  5481  frsn  5483  eqrelriv  5506  relsnb  5519  relopabiALT  5539  opabid2  5544  ididg  5568  iss  5742  ord0eln0  6077  sucidg  6101  nsuceq0  6103  onun2i  6138  funopg  6216  fn0  6303  f00  6384  f0bi  6385  f10d  6471  f1o00  6472  fo00  6473  brprcneu  6485  dffn5  6548  fsn  6714  funop  6728  funsndifnop  6730  fnsnb  6745  eufnfv  6811  f1eqcocnv  6876  nfriotad  6939  riotaprop  6955  oprabid  7001  elrnmpo  7097  ov6g  7122  ovelrn  7134  caovmo  7195  offn  7232  caofinvl  7248  fr3nr  7304  onprc  7309  ordeleqon  7313  onint0  7321  0elsuc  7360  onuninsuci  7365  orduninsuc  7368  ordzsl  7370  onzsl  7371  tfinds  7384  limomss  7395  limom  7405  peano5  7414  xpexr  7432  eqop2  7538  opreuopreu  7540  1stconst  7597  2ndconst  7598  funsssuppss  7653  dftpos3  7707  dftpos4  7708  wfrlem4  7755  wfrlem4OLD  7756  wfrlem14  7766  oawordeulem  7975  omwordi  7992  nnmwordi  8056  riiner  8164  ecopover  8195  map0g  8241  mapsnd  8242  elixpsn  8292  en0  8363  en1  8367  fiprc  8386  sbthlem2  8418  sbthlem4  8420  sbthlem5  8421  nneneq  8490  sdom1  8507  fineqvlem  8521  nfielex  8536  findcard  8546  findcard2  8547  elfiun  8683  marypha1lem  8686  oicl  8782  oif  8783  oion  8789  hartogslem1  8795  hartogs  8797  wemapso2  8806  card2on  8807  0wdom  8823  brwdom2  8826  inf3lem6  8884  cantnflem3  8942  cantnflem4  8943  wemapwe  8948  cnfcom  8951  tctr  8970  r1tr  8993  r1rankidb  9021  r1pw  9062  scottex  9102  scott0  9103  bnd2  9110  eldju2ndl  9141  tskwe  9167  oncard  9177  cardlim  9189  harsdom  9212  en2eleq  9222  dfac8alem  9243  cardaleph  9303  iunfictbso  9328  infmap2  9432  ackbij1lem18  9451  cff  9462  cfsuc  9471  cff1  9472  cflim2  9477  cfss  9479  sdom2en01  9516  infpssrlem4  9520  fin23lem7  9530  fin23lem11  9531  isfin2-2  9533  fin23lem26  9539  fin23lem19  9550  fin23lem17  9552  isf34lem2  9587  isf34lem4  9591  fin1a2lem6  9619  fin1a2lem10  9623  fin1a2lem12  9625  itunifn  9631  hsmexlem1  9640  axcc2lem  9650  dcomex  9661  axdc3lem4  9667  ondomon  9777  konigthlem  9782  pwcfsdom  9797  cfpwsdom  9798  axpowndlem3  9813  canth4  9861  canthnumlem  9862  canthwelem  9864  canthwe  9865  canthp1lem2  9867  pwfseqlem4  9876  pwfseqlem5  9877  gchaleph  9885  gch2  9889  winainflem  9907  0tsk  9969  rankcf  9991  tskcard  9995  gruina  10032  grutsk  10036  tskmid  10054  indpi  10121  nqereu  10143  mulcanenq  10174  recmulnq  10178  archnq  10194  ltsopr  10246  1ne0sr  10310  0idsr  10311  00sr  10313  leid  10530  lelttric  10541  divcan3  11119  lemul1a  11289  nn1suc  11456  nn0n0n1ge2b  11769  xnn0xr  11778  xnn0nemnf  11784  nn0lt10b  11851  nn0ind-raph  11889  elnn1uz2  12133  indstr2  12135  uzsupss  12148  rpnnen1lem4  12188  rpnnen1lem5  12189  xrnemnf  12323  xrnepnf  12324  mnfltxr  12333  xnn0n0n1ge2b  12337  xnn0ge0  12339  xrlttri  12343  xrlttr  12344  xrleid  12355  qbtwnxr  12404  xmullem2  12468  xlemul1a  12491  xrub  12515  reltxrnmnf  12545  ixxun  12564  xnn0xrge0  12701  fztpval  12779  fseq1p1m1  12791  elfznelfzob  12952  ltweuz  13138  fzfi  13149  fsuppmapnn0fiubex  13169  ser0f  13232  0exp  13273  faclbnd4lem1  13462  bcn1  13482  hashnemnf  13513  hashv01gt1  13514  hashsnle1  13585  hashgt12el2  13591  hashpw  13604  hashf1  13622  fz1isolem  13626  hash2prb  13635  wrdlndmOLD  13685  0wrd0  13695  wrdlen1  13711  ccatvalfn  13738  wrdl1exs1  13770  swrdlen  13806  swrdwrdsymb  13833  swrdspsleq  13836  cats1un  13908  wrdind  13909  wrdindOLD  13910  wrd2ind  13911  wrd2indOLD  13912  swrdccatin1  13918  repswsymballbi  13993  cshw1  14040  scshwfzeqfzo  14044  wrdl2exs2  14164  trclfvcotr  14224  relexp1g  14240  relexp0rel  14251  relexprelg  14252  sqr0lem  14455  sqrtsq  14484  mptfzshft  14987  prodf1f  15102  fprodrev  15185  egt2lt3  15413  0dvds  15484  nn0onn  15585  nn0o  15588  divalgmod  15611  flodddiv4  15618  bitsp1o  15636  gcddvds  15706  bezout  15741  lcmdvds  15802  rpdvds  15854  1nprm  15873  prmind2  15879  nnoddn2prmb  16000  pcpre1  16029  vdwapf  16158  vdwapid1  16161  ram0  16208  ramz  16211  prmolefac  16232  cshws0  16285  prmlem0  16289  strle1  16442  restsspw  16555  prdsdsfn  16588  imasdsfn  16637  imasaddfnlem  16651  imasvscafn  16660  xpscfv  16685  xpsfrnel  16686  isacs1i  16780  cidfn  16802  fnhomeqhomf  16813  comffn  16827  isoval  16887  sscres  16945  cofucl  17010  idffth  17055  ressffth  17060  catcoppccl  17220  estrchomfn  17237  funcestrcsetclem4  17245  funcestrcsetclem7  17248  equivestrcsetc  17254  funcsetcestrclem4  17260  funcsetcestrclem7  17263  1stfcl  17299  2ndfcl  17300  prfcl  17305  evlfcl  17324  curf1cl  17330  curfcl  17334  hofcl  17361  yonedainv  17383  pospo  17435  lubfun  17442  glbfun  17455  joindmss  17469  meetdmss  17483  ipopos  17622  acsficl2d  17638  dirref  17697  mgmidcl  17727  mgmlrid  17728  cntzssv  18223  symggrp  18283  symgid  18284  idresperm  18292  pmtrfmvdn0  18345  symggen  18353  psgnunilem1  18376  psgnprfval  18405  slwpgp  18493  frgpmhm  18645  frgpuptinv  18651  frgpup3lem  18657  gsumzoppg  18811  gsumcom2  18842  abv0  19318  rrgsupp  19779  psrvscafval  19878  psrridm  19892  ltbwe  19960  psrbag0  19981  psrbagsn  19982  subrgascl  19985  zrhrhm  20355  psgnodpmr  20430  frlmphl  20621  ellspd  20642  mattpostpos  20761  mavmul0  20859  mavmul0g  20860  mdet0f1o  20900  m1detdiag  20904  m2detleiblem5  20932  m2detleiblem6  20933  m2detleiblem3  20936  m2detleiblem4  20937  maducoeval2  20947  d1mat2pmat  21045  chpmat1dlem  21141  chpmat1d  21142  baspartn  21260  eltg3  21268  topnex  21302  fctop  21310  cctop  21312  discld  21395  mretopd  21398  neipeltop  21435  neitr  21486  restcls  21487  ordtbaslem  21494  ordtuni  21496  idcn  21563  cnrmi  21666  cmpsublem  21705  cmpsub  21706  tgcmp  21707  uncmp  21709  hauscmplem  21712  cmpfi  21714  bwth  21716  1stcrestlem  21758  disllycmp  21804  dis1stc  21805  refref  21819  kgeni  21843  1stckgenlem  21859  kqffn  22031  snfil  22170  filconn  22189  cfinfil  22199  ufileu  22225  filufint  22226  fixufil  22228  cfinufil  22234  ufilen  22236  fin1aufil  22238  fmf  22251  rnelfm  22259  flimclslem  22290  hauspwpwf1  22293  supnfcls  22326  flimfnfcls  22334  fclscmp  22336  alexsubALTlem2  22354  alexsubALTlem3  22355  alexsubALT  22357  ptcmplem1  22358  cnextrel  22369  tsmsfbas  22433  ustref  22524  trust  22535  restutop  22543  isusp  22567  xmet0  22649  imasdsf1olem  22680  blfvalps  22690  blfps  22713  blf  22714  restmetu  22877  dscmet  22879  isngp2  22903  nm0  22935  nrginvrcn  22998  nmoix  23035  qdensere  23075  iccconn  23135  iccpnfcnv  23245  xrhmeo  23247  lebnumlem3  23264  metsscmetcld  23615  bcthlem5  23628  csschl  23676  rrxmfval  23706  minveclem3b  23728  cniccbdd  23759  ovolicc2lem4  23818  iunmbl  23851  ioorinv  23874  ioorcl  23875  i1f1lem  23987  limcvallem  24166  ellimc2  24172  limccnp  24186  limccnp2  24187  limcco  24188  perfdvf  24198  recnprss  24199  fncpn  24227  dvcmulf  24239  c1lip1  24291  lhop2  24309  q1pcl  24446  r1pdeglt  24449  ply1remlem  24453  plyssc  24487  ulm0  24676  cxpeq0  24956  cxplea  24974  cxplogb  25059  asinlem  25141  isppw2  25388  muval2  25407  dchrfi  25527  dchrpt  25539  bposlem6  25561  lgsdir2lem2  25598  lgsqr  25623  gausslemma2dlem4  25641  2lgslem2  25667  2lgslem3  25676  2lgs  25679  2sqlem7  25696  2sqlem11  25701  chtppilim  25747  tgldimor  25984  tgcgr4  26013  tglnfn  26029  tglnunirn  26030  mirne  26149  mircinv  26150  perpln1  26192  perpln2  26193  lmiisolem  26278  xmstrkgc  26369  axcgrtr  26398  axsegconlem9  26408  axlowdimlem5  26429  axlowdimlem17  26441  axlowdim1  26442  uhgr0e  26553  edglnl  26625  uhgr0edgfi  26719  issubgr2  26751  subgrprop2  26753  egrsubgr  26756  0grsubgr  26757  0uhgrsubgr  26758  uhgrsubgrself  26759  nbgr0vtx  26835  nbgr1vtx  26837  nbgrssovtx  26840  nb3grprlem1  26859  uvtx01vtx  26876  cplgr1vlem  26908  cplgr1v  26909  usgrexilem  26919  wlkcomp  27109  wlk1walk  27117  wlkp1lem5  27159  uhgrwkspthlem1  27236  pthdlem1  27249  clwlkcomp  27262  lfgrn1cycl  27285  uspgrn2crct  27288  wwlksn0s  27341  umgrwwlks2on  27457  clwwlkn  27535  clwwlkn1  27551  0ewlk  27637  1ewlk  27638  0spth  27649  upgr1wlkdlem2  27669  wlk2v2e  27680  upgr3v3e3cycl  27703  upgr4cycl4dv4e  27708  eupth0  27737  frgr0v  27789  frgr1v  27799  1vwmgr  27804  ex-opab  27983  grpoinvf  28080  nvmid  28207  nmlnoubi  28344  hiidrcl  28645  hsn0elch  28798  shjshseli  29045  cmbr4i  29153  dfiop2  29305  kbpj  29508  nmopun  29566  adjeq0  29643  kbass2  29669  pjssdif1i  29727  pjinvari  29743  pjcmul2i  29754  pj3i  29760  stge1i  29790  stle0i  29791  sumdmdlem2  29971  dmdbr6ati  29975  dmdbr7ati  29976  rabsnel  30036  disjdifprg  30085  ofoprabco  30165  padct  30208  fpwrelmapffslem  30221  xrlelttric  30229  xnn0gt0  30247  iundisj2cnt  30272  f1ocnt  30273  fz1nnct  30274  fz1nntr  30275  hashxpe  30277  dvdszzq  30278  nn0min  30284  xrge0tsmsbi  30531  locfinref  30749  dispcmp  30767  pstmxmet  30781  xrge0iifcnv  30820  xrge0iif1  30825  qqhre  30905  esumcl  30933  esumpr2  30970  esumpinfval  30976  esumpcvgval  30981  ofcfn  31003  pwsiga  31034  prsiga  31035  sigainb  31040  ldgenpisyslem1  31067  measiuns  31121  relfae  31151  pmeasmono  31227  sitgf  31250  eulerpartgbij  31275  sgnmulsgn  31453  sgnmulsgp  31454  signswch  31477  signslema  31478  signstlen  31483  circlevma  31561  bnj216  31650  bnj151  31796  bnj517  31804  bnj970  31866  bnj1145  31910  bnj1498  31978  subfacp1lem5  32016  erdszelem8  32030  kur14lem1  32038  indispconn  32066  cvmsss2  32106  satf00  32184  satf0suclem  32185  fmlasuc0  32194  msubrn  32296  dfpo2  32511  dfon2lem7  32554  nosgnn0i  32687  nolesgn2ores  32700  nosepnelem  32705  nosepdmlem  32708  nosupbnd1lem3  32731  nosupbnd1lem5  32733  nosupbnd2lem1  32736  brbigcup  32880  elsingles  32900  fnimage  32911  funpartlem  32924  dfrdg4  32933  imagesset  32935  altopthsn  32943  elaltxp  32957  ellines  33134  linethru  33135  rankeq1o  33153  elhf2  33157  hfninf  33168  nn0prpwlem  33191  fneref  33219  neibastop2lem  33229  limsucncmpi  33313  bj-exlimmpbir  33722  curryset  33752  bj-snglex  33803  bj-restpw  33893  bj-inftyexpidisj  33961  topdifinffinlem  34070  relowlssretop  34086  rdgeqoa  34093  finxpreclem6  34118  fvineqsneq  34134  pibt2  34139  poimirlem23  34356  poimirlem29  34362  poimirlem31  34364  volsupnfl  34378  cnambfre  34381  dvasin  34419  dvacos  34420  sdclem2  34459  sstotbnd2  34494  ssbnd  34508  ismgmOLD  34570  grpokerinj  34613  rngomndo  34655  isdrngo1  34676  ac6s6  34894  iss2  35047  cnvelrels  35180  cosselrels  35181  brssrid  35187  brcnvssrid  35192  dfdisjs5  35390  eldisjs5  35404  prtlem12  35448  riotasv2d  35538  lkrscss  35679  islshpkrN  35701  isline  36320  ispointN  36323  0psubN  36330  linepsubN  36333  atpsubN  36334  cdlemk36  37494  diafn  37615  dibfna  37735  dibvalrel  37744  dicvalrelN  37766  diclspsn  37775  dihvalrel  37860  dih1  37867  lclkrlem1  38087  lclkr  38114  mapd1o  38229  mapdin  38243  hdmapfnN  38410  hgmapfnN  38469  repncan2  38645  elrfirn  38687  ismrcd1  38690  istopclsd  38692  rabren3dioph  38808  jm2.17b  38954  jm2.22  38988  jm2.23  38989  ttac  39029  pw2f1ocnv  39030  dnnumch1  39040  hbtlem5  39124  mncn0  39135  aaitgo  39158  rngunsnply  39169  clcnvlem  39346  relexp01min  39421  ntrf  39836  ssrecnpr  40056  seff  40057  sblpnf  40058  nzss  40065  dvconstbi  40082  ipo0  40200  ifr0  40201  addrfn  40223  subrfn  40224  mulvfn  40225  refsum2cnlem1  40713  ellimciota  41326  dvmptconst  41629  dvmptidg  41631  dvmulcncf  41640  dvdivcncf  41642  stoweidlem26  41742  stoweidlem50  41766  stoweidlem57  41773  aiotaval  42699  ndfatafv2nrn  42826  afv2ndefb  42829  funop1  42888  fun2dmnopgexmpl  42889  2ffzoeq  42934  iccpartiltu  42954  iccpartigtl  42955  zofldiv2ALTV  43195  evenprm2  43247  9fppr8  43270  stgoldbwt  43309  nnsum3primesle9  43327  nnsum4primeseven  43333  nnsum4primesevenALTV  43334  tgblthelfgott  43348  isomgreqve  43358  uspgrex  43393  0mgm  43409  nnsgrpmgm  43451  c0snmhm  43550  rngchomffvalALTV  43630  funcringcsetcALTV2lem4  43674  funcringcsetclem4ALTV  43697  srhmsubc  43711  rhmsubclem1  43721  srhmsubcALTV  43729  rhmsubcALTVlem1  43739  mapsnop  43757  zlmodzxzldeplem4  43925  zofldiv2  43959  fdivval  43967  nnlog2ge0lt1  43994  dig1  44036