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  2392  nfald2  2443  nfabd2  2915  raleleq  3306  raleleqOLD  3307  ceqsexv2d  3490  dedhb  3665  csbie2df  4396  ssdifeq0  4440  r19.2zb  4449  dedth  4537  pwidg  4573  snidg  4614  rexreusng  4633  exsnrex  4634  ifpr  4647  rmosn  4673  rabrsn  4678  prid1g  4714  tpid1g  4723  tpid2g  4725  tpid3g  4726  pwpw0  4767  sssn  4780  elpreqpr  4821  unimax  4897  intmin3  4929  eqbrtrdi  5134  al0ssb  5250  rabelpw  5278  intabs  5291  difelpw  5296  0inp0  5301  axpr  5369  intidg  5404  copsexgw  5437  copsexg  5438  euotd  5460  elopab  5474  elvvuni  5700  posn  5709  frsn  5711  eqrelriv  5736  relsnb  5749  relopabiALT  5770  opabid2  5775  ididg  5800  iss  5990  dfpo2  6248  ord0eln0  6367  sucidg  6394  nsuceq0  6396  funopg  6520  fn0  6617  f00  6710  f0bi  6711  f10d  6802  f1o00  6803  fo00  6804  brprcneu  6816  brprcneuALT  6817  dffn5  6885  fsn  7073  funop  7087  funsndifnop  7089  fnsnbOLD  7106  eufnfv  7169  f1ounsn  7213  f1eqcocnv  7242  nfriotadw  7318  nfriotad  7321  riotaprop  7337  oprabidw  7384  oprabid  7385  elrnmpo  7489  ov6g  7517  ovelrn  7529  caovmo  7590  offn  7630  caofinvl  7649  fr3nr  7712  onprc  7718  ordeleqon  7722  onint0  7731  0elsuc  7774  onuninsuci  7780  orduninsuc  7783  ordzsl  7785  onzsl  7786  tfinds  7800  limomss  7811  limom  7822  peano5  7833  xpexr  7858  eqop2  7974  opreuopreu  7976  1stconst  8040  2ndconst  8041  frxp2  8084  frxp3  8091  funsssuppss  8130  dftpos3  8184  dftpos4  8185  oawordeulem  8479  omwordi  8496  nnmwordi  8560  riiner  8724  ecopover  8755  map0g  8818  mapsnd  8820  elixpsn  8871  en0  8950  en0ALT  8951  en0r  8952  en1  8956  snfi  8975  fiprc  8977  sbthlem2  9012  sbthlem4  9014  sbthlem5  9015  0domg  9028  findcard  9087  findcard2  9088  nneneq  9130  sdom1  9149  1sdom2dom  9153  fineqvlem  9167  nfielex  9176  enp1i  9182  elfiun  9339  marypha1lem  9342  oicl  9440  oif  9441  oion  9447  hartogslem1  9453  hartogs  9455  wemapso2  9464  card2on  9465  0wdom  9481  brwdom2  9484  inf3lem6  9548  cantnflem3  9606  cantnflem4  9607  wemapwe  9612  cnfcom  9615  ssttrcl  9630  ttrclselem2  9641  tctr  9655  r1tr  9691  r1rankidb  9719  r1pw  9760  scottex  9800  scott0  9801  bnd2  9808  eldju2ndl  9839  tskwe  9865  oncard  9875  cardlim  9887  harsdom  9910  en2eleq  9921  dfac8alem  9942  cardaleph  10002  iunfictbso  10027  infmap2  10130  ackbij1lem18  10149  cff  10161  cfsuc  10170  cff1  10171  cflim2  10176  cfss  10178  sdom2en01  10215  infpssrlem4  10219  fin23lem7  10229  fin23lem11  10230  isfin2-2  10232  fin23lem26  10238  fin23lem19  10249  fin23lem17  10251  isf34lem2  10286  isf34lem4  10290  fin1a2lem6  10318  fin1a2lem10  10322  fin1a2lem12  10324  itunifn  10330  hsmexlem1  10339  axcc2lem  10349  dcomex  10360  axdc3lem4  10366  ondomon  10476  konigthlem  10481  pwcfsdom  10496  cfpwsdom  10497  axpowndlem3  10512  canth4  10560  canthnumlem  10561  canthwelem  10563  canthwe  10564  canthp1lem2  10566  pwfseqlem4  10575  pwfseqlem5  10576  gchaleph  10584  gch2  10588  winainflem  10606  0tsk  10668  rankcf  10690  tskcard  10694  gruina  10731  grutsk  10735  tskmid  10753  indpi  10820  nqereu  10842  mulcanenq  10873  recmulnq  10877  archnq  10893  ltsopr  10945  1ne0sr  11009  0idsr  11010  00sr  11012  leid  11230  lelttric  11241  divcan3  11823  divid  11828  div0  11830  lemul1a  11996  nn1suc  12168  nn0n0n1ge2b  12471  xnn0xr  12480  xnn0nemnf  12486  nn0lt10b  12556  nn0ind-raph  12594  elnn1uz2  12844  indstr2  12846  uzsupss  12859  rpnnen1lem4  12899  rpnnen1lem5  12900  xrnemnf  13037  xrnepnf  13038  mnfltxr  13047  xnn0n0n1ge2b  13052  xnn0ge0  13054  xrlttri  13059  xrlttr  13060  xrleid  13071  qbtwnxr  13120  xmullem2  13185  xlemul1a  13208  xrub  13232  reltxrnmnf  13263  ixxun  13282  xnn0xrge0  13427  fztpval  13507  fseq1p1m1  13519  elfznelfzob  13694  ltweuz  13886  fzfi  13897  fsuppmapnn0fiubex  13917  ser0f  13980  0exp  14022  faclbnd4lem1  14218  bcn1  14238  hashnemnf  14269  hashv01gt1  14270  hashsnle1  14342  hashgt12el2  14348  hashpw  14361  hashf1  14382  fz1isolem  14386  hash2prb  14397  hash3tpb  14420  0wrd0  14465  wrdlen1  14479  ccatvalfn  14506  eqs1  14537  wrdl1exs1  14538  swrdlen  14572  swrdwrdsymb  14587  swrdspsleq  14590  cats1un  14645  wrdind  14646  wrd2ind  14647  swrdccatin1  14649  repswsymballbi  14704  cshw1  14746  scshwfzeqfzo  14751  wrdl2exs2  14871  trclfvcotr  14934  relexp1g  14951  relexp0rel  14962  relexprelg  14963  relexpreld  14965  sqrt0  15166  sqrtsq  15194  mptfzshft  15703  prodf1f  15817  egt2lt3  16133  0dvds  16205  nn0onn  16309  nn0o  16312  divalgmod  16335  flodddiv4  16344  bitsp1o  16362  gcddvds  16432  bezout  16472  lcmdvds  16537  rpdvds  16589  1nprm  16608  prmind2  16614  dvdszzq  16650  nnoddn2prmb  16743  pcpre1  16772  vdwapf  16902  vdwapid1  16905  ram0  16952  ramz  16955  prmolefac  16976  cshws0  17031  prmlem0  17035  strle1  17087  restsspw  17353  prdsdsfn  17387  imasdsfn  17436  imasaddfnlem  17450  imasvscafn  17459  xpsfrnel  17484  isacs1i  17581  cidfn  17603  fnhomeqhomf  17615  comffn  17629  isoval  17690  sscres  17748  cofucl  17813  idffth  17860  ressffth  17865  cat1lem  18021  catcoppccl  18042  estrchomfn  18059  funcestrcsetclem4  18067  funcestrcsetclem7  18070  equivestrcsetc  18076  funcsetcestrclem4  18082  funcsetcestrclem7  18085  1stfcl  18121  2ndfcl  18122  prfcl  18127  evlfcl  18146  curf1cl  18152  curfcl  18156  hofcl  18183  yonedainv  18205  pospo  18267  lubfun  18274  glbfun  18287  joindmss  18301  meetdmss  18315  ipopos  18460  acsficl2d  18476  dirref  18525  mgmidcl  18558  mgmlrid  18559  ielefmnd  18779  smndex1basss  18797  smndex1n0mnd  18804  cntzssv  19225  idresperm  19283  symgvalstruct  19294  pmtrfmvdn0  19359  symggen  19367  psgnunilem1  19390  psgnprfval  19418  slwpgp  19510  frgpmhm  19662  frgpuptinv  19668  frgpup3lem  19674  gsumzoppg  19841  gsumcom2  19872  c0snmhm  20366  srhmsubc  20583  rhmsubclem1  20588  rrgsupp  20604  abv0  20726  zrhrhm  21436  psgnodpmr  21515  frlmphllem  21705  ellspd  21727  psrvscafval  21873  psrridm  21888  ltbwe  21967  psrbag0  21985  psrbagsn  21986  subrgascl  21989  psdmul  22069  mattpostpos  22357  mavmul0  22455  mavmul0g  22456  mdet0f1o  22496  m1detdiag  22500  m2detleiblem5  22528  m2detleiblem6  22529  m2detleiblem3  22532  m2detleiblem4  22533  maducoeval2  22543  d1mat2pmat  22642  chpmat1dlem  22738  chpmat1d  22739  baspartn  22857  eltg3  22865  topnex  22899  fctop  22907  cctop  22909  discld  22992  mretopd  22995  neipeltop  23032  neitr  23083  restcls  23084  ordtbaslem  23091  ordtuni  23093  idcn  23160  cnrmi  23263  cmpsublem  23302  cmpsub  23303  tgcmp  23304  uncmp  23306  hauscmplem  23309  cmpfi  23311  bwth  23313  1stcrestlem  23355  disllycmp  23401  dis1stc  23402  refref  23416  kgeni  23440  1stckgenlem  23456  kqffn  23628  snfil  23767  filconn  23786  cfinfil  23796  ufileu  23822  filufint  23823  fixufil  23825  cfinufil  23831  ufilen  23833  fin1aufil  23835  fmf  23848  rnelfm  23856  flimclslem  23887  hauspwpwf1  23890  supnfcls  23923  flimfnfcls  23931  fclscmp  23933  alexsubALTlem2  23951  alexsubALTlem3  23952  alexsubALT  23954  ptcmplem1  23955  cnextrel  23966  tsmsfbas  24031  ustref  24122  trust  24133  restutop  24141  isusp  24165  xmet0  24246  imasdsf1olem  24277  blfvalps  24287  blfps  24310  blf  24311  restmetu  24474  dscmet  24476  isngp2  24501  nm0  24533  nrginvrcn  24596  nmoix  24633  qdensere  24673  iccconn  24735  iccpnfcnv  24858  xrhmeo  24860  lebnumlem3  24878  metsscmetcld  25231  bcthlem5  25244  csschl  25292  rrxmfval  25322  minveclem3b  25344  cniccbdd  25378  ovolicc2lem4  25437  iunmbl  25470  ioorinv  25493  ioorcl  25494  i1f1lem  25606  limcvallem  25788  ellimc2  25794  limccnp  25808  limccnp2  25809  limcco  25810  perfdvf  25820  recnprss  25821  fncpn  25851  dvcmulf  25864  c1lip1  25918  lhop2  25936  q1pcl  26078  r1pdeglt  26081  ply1remlem  26086  plyssc  26121  ulm0  26316  cxpeq0  26603  cxplea  26621  cxplogb  26712  asinlem  26794  isppw2  27041  muval2  27060  dchrfi  27182  dchrpt  27194  bposlem6  27216  lgsdir2lem2  27253  lgsqr  27278  gausslemma2dlem4  27296  2lgslem2  27322  2lgslem3  27331  2lgs  27334  2sqlem7  27351  2sqlem11  27356  chtppilim  27402  nosgnn0i  27587  nolesgn2ores  27600  nogesgn1ores  27602  nosepnelem  27607  nosepdmlem  27611  nosupbnd1lem3  27638  nosupbnd1lem5  27640  nosupbnd2lem1  27643  noinfbnd1lem3  27653  noinfbnd1lem5  27655  noinfbnd2lem1  27658  oldval  27782  made0  27805  lrrecpo  27871  pncan2s  28001  divscan3d  28161  abssor  28171  om2noseqfo  28215  noseqrdglem  28222  noseqrdgfn  28223  noseqrdg0  28224  onsfi  28270  nohalf  28334  expsne0  28346  pw2divscan3d  28351  tgldimor  28465  tgcgr4  28494  tglnfn  28510  tglnunirn  28511  mirne  28630  mircinv  28631  perpln1  28673  perpln2  28674  lmiisolem  28759  xmstrkgc  28849  axcgrtr  28878  axsegconlem9  28888  axlowdimlem5  28909  axlowdimlem17  28921  axlowdim1  28922  uhgr0e  29034  edglnl  29106  uhgr0edgfi  29203  issubgr2  29235  subgrprop2  29237  egrsubgr  29240  0grsubgr  29241  0uhgrsubgr  29242  uhgrsubgrself  29243  nbgr1vtx  29321  nbgrssovtx  29324  nb3grprlem1  29343  uvtx01vtx  29360  cplgr1vlem  29392  cplgr1v  29393  usgrexilem  29403  wlkcomp  29594  wlk1walk  29602  wlkp1lem5  29639  uhgrwkspthlem1  29716  pthdlem1  29729  clwlkcomp  29742  lfgrn1cycl  29768  uspgrn2crct  29771  wwlksn0s  29824  umgrwwlks2on  29920  clwwlkn  29988  clwwlkn1  30003  0ewlk  30076  1ewlk  30077  0spth  30088  upgr1wlkdlem2  30108  wlk2v2e  30119  upgr3v3e3cycl  30142  upgr4cycl4dv4e  30147  eupth0  30176  frgr0v  30224  frgr1v  30233  1vwmgr  30238  ex-opab  30394  grpoinvf  30494  nvmid  30621  nmlnoubi  30758  hiidrcl  31057  hsn0elch  31210  shjshseli  31455  cmbr4i  31563  dfiop2  31715  kbpj  31918  nmopun  31976  adjeq0  32053  kbass2  32079  pjssdif1i  32137  pjinvari  32153  pjcmul2i  32164  pj3i  32170  stge1i  32200  stle0i  32201  sumdmdlem2  32381  dmdbr6ati  32385  dmdbr7ati  32386  rabsnel  32462  unidifsnel  32497  unidifsnne  32498  disjdifprg  32537  ofoprabco  32621  padct  32676  fpwrelmapffslem  32688  xrlelttric  32708  xnn0gt0  32725  iundisj2cnt  32755  f1ocnt  32758  fz1nnct  32759  fz1nntr  32760  hashxpe  32765  nn0min  32778  sgnmulsgn  32800  sgnmulsgp  32801  wrdt2ind  32908  xrge0tsmsbi  33029  opprabs  33429  rtelextdg2lem  33692  2sqr3minply  33746  locfinref  33807  dispcmp  33825  zartopn  33841  zarcmplem  33847  pstmxmet  33863  xrge0iifcnv  33899  xrge0iif1  33904  qqhre  33986  esumcl  33996  esumpr2  34033  esumpinfval  34039  esumpcvgval  34044  ofcfn  34066  pwsiga  34096  prsiga  34097  sigainb  34102  ldgenpisyslem1  34129  measiuns  34183  relfae  34213  pmeasmono  34291  sitgf  34314  eulerpartgbij  34339  signswch  34528  signslema  34529  signstlen  34534  signstfvn  34536  circlevma  34609  bnj216  34698  bnj151  34843  bnj517  34851  bnj970  34913  bnj1145  34959  bnj1498  35027  fineqvrep  35069  fineqvac  35071  wevgblacfn  35081  0nn0m1nnn0  35085  pthhashvtx  35100  acycgr0v  35120  prclisacycgr  35123  umgracycusgr  35126  cusgracyclt3v  35128  subfacp1lem5  35156  erdszelem8  35170  kur14lem1  35178  indispconn  35206  cvmsss2  35246  satfvsuclem2  35332  satfrel  35339  satfrnmapom  35342  satfv0fun  35343  satf00  35346  satf0suclem  35347  fmlasuc0  35356  msubrn  35501  dfon2lem7  35762  brbigcup  35871  elsingles  35891  fnimage  35902  funpartlem  35915  dfrdg4  35924  imagesset  35926  altopthsn  35934  elaltxp  35948  ellines  36125  linethru  36126  rankeq1o  36144  elhf2  36148  hfninf  36159  nn0prpwlem  36295  fneref  36323  neibastop2lem  36333  limsucncmpi  36418  bj-exlimmpbir  36887  curryset  36919  bj-snglex  36946  bj-restpw  37065  bj-inftyexpidisj  37183  topdifinffinlem  37320  relowlssretop  37336  rdgeqoa  37343  finxpreclem6  37369  fvineqsneq  37385  pibt2  37390  poimirlem23  37622  poimirlem29  37628  poimirlem31  37630  volsupnfl  37644  cnambfre  37647  dvasin  37683  dvacos  37684  sdclem2  37721  sstotbnd2  37753  ssbnd  37767  ismgmOLD  37829  grpokerinj  37872  rngomndo  37914  isdrngo1  37935  ac6s6  38151  iss2  38311  cnvelrels  38471  cosselrels  38472  brssrid  38478  brcnvssrid  38483  dfdisjs5  38689  eldisjs5  38703  mpets2  38818  pets  38829  prtlem12  38845  riotasv2d  38935  lkrscss  39076  islshpkrN  39098  isline  39718  ispointN  39721  0psubN  39728  linepsubN  39731  atpsubN  39732  cdlemk36  40892  diafn  41013  dibfna  41133  dibvalrel  41142  dicvalrelN  41164  diclspsn  41173  dihvalrel  41258  dih1  41265  lclkrlem1  41485  lclkr  41512  mapd1o  41627  mapdin  41641  hdmapfnN  41808  hgmapfnN  41867  lcmineqlem10  42011  sticksstones9  42127  sn-iotalem  42194  readvrec2  42334  readvrec  42335  repncan2  42355  elrfirn  42668  ismrcd1  42671  istopclsd  42673  rabren3dioph  42788  jm2.17b  42934  jm2.22  42968  jm2.23  42969  ttac  43009  pw2f1ocnv  43010  dnnumch1  43017  hbtlem5  43101  mncn0  43112  aaitgo  43135  rngunsnply  43142  unielss  43191  onexlimgt  43216  cantnfresb  43297  dflim5  43302  naddwordnexlem4  43374  safesnsupfiss  43388  safesnsupfidom1o  43390  safesnsupfilb  43391  ensucne0OLD  43503  clcnvlem  43596  relexp01min  43686  ntrf  44096  ssrecnpr  44281  seff  44282  sblpnf  44283  nzss  44290  dvconstbi  44307  ipo0  44422  ifr0  44423  addrfn  44445  subrfn  44446  mulvfn  44447  wfaxrep  44968  refsum2cnlem1  45015  rn1st  45251  ellimciota  45596  dvmptconst  45897  dvmptidg  45899  dvmulcncf  45907  dvdivcncf  45909  stoweidlem26  46008  stoweidlem50  46032  stoweidlem57  46039  aiotaval  47080  ndfatafv2nrn  47206  afv2ndefb  47209  funop1  47268  fun2dmnopgexmpl  47269  2ffzoeq  47312  2ltceilhalf  47313  m1modne  47333  iccpartiltu  47407  iccpartigtl  47408  zofldiv2ALTV  47647  evenprm2  47699  9fppr8  47722  stgoldbwt  47761  nnsum3primesle9  47779  nnsum4primeseven  47785  nnsum4primesevenALTV  47786  tgblthelfgott  47800  dfclnbgr6  47840  cycl3grtri  47930  grtrimap  47931  stgredgel  47940  stgr1  47944  isubgr3stgrlem2  47950  isubgr3stgrlem3  47951  usgrexmpl2trifr  48012  gpg5nbgrvtx13starlem1  48046  gpg5nbgrvtx13starlem2  48047  gpg5nbgrvtx13starlem3  48048  gpg5nbgr3star  48056  gpg3kgrtriex  48064  uspgrex  48122  0mgm  48138  nnsgrpmgm  48148  rngchomffvalALTV  48250  rhmsubcALTVlem1  48253  funcringcsetcALTV2lem4  48265  funcringcsetclem4ALTV  48288  srhmsubcALTV  48297  mapsnop  48316  zlmodzxzldeplem4  48476  zofldiv2  48504  fdivval  48512  nnlog2ge0lt1  48539  dig1  48581  itcoval2  48637  itcoval3  48638  mosn  48785  mo0  48786  mof02  48811  mofeu  48820  f102g  48824  f1mo  48825  tposres0  48849  f1omo  48865  f1omoOLD  48866  resipos  48947  intubeu  48956  unilbeu  48957  sectfn  49002  nelsubclem  49040  idfu1stf1o  49072  imaidfu  49083  oppfvallem  49108  funcoppc3  49120  idfth  49131  idsubc  49133  uptposlem  49170  swapf2fn  49241  swapf1f1o  49248  swapf2f1o  49249  swapf2f1oaALT  49251  fucof1  49295  fucofn2  49297  fucofn22  49313  reldmprcof1  49354  reldmprcof2  49355  fucoppcid  49381  fucoppc  49383  functhinclem1  49417  fullthinc  49423  thincciso  49426  indcthing  49433  indthinc  49435  indthincALT  49436  functermc  49481  discsntermlem  49543  reldmlan2  49590  reldmran2  49591  rellan  49596  relran  49597  termolmd  49643