Theorem mpbiri 261

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

Syntax hints:   → wi 4   ↔ wb 209

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 210

This theorem is referenced by:  elimh  1097  spei  2428  nfald2  2479  nfabd2  2950  raleleq  3335  raleleqOLD  3336  ceqsexv2d  3506  dedhb  3669  csbie2df  4400  ssdifeq0  4443  dedth  4542  pwidgOLD  4579  snidg  4622  rexreusng  4641  exsnrex  4642  ifpr  4655  rmosn  4681  rabrsn  4686  prid1g  4722  tpid1g  4731  tpid2g  4733  tpid3g  4734  pwpw0  4774  sssn  4787  elpreqpr  4828  unimax  4906  intmin3  4937  eqbrtrdi  5144  al0ssb  5263  vneqv  5271  rabelpw  5297  intabs  5310  difelpw  5315  0inp0  5320  axpr  5389  intidg  5429  copsexgw  5463  copsexgwOLD  5464  copsexg  5465  euotd  5487  elopab  5502  elvvuni  5729  posn  5738  frsn  5740  eqrelriv  5766  relsnb  5780  relopabiALT  5801  opabid2  5806  ididg  5830  iss  6028  dfpo2  6287  ord0eln0  6406  sucidg  6433  nsuceq0  6435  funopg  6559  fn0  6656  f00  6750  f0bi  6751  f10d  6845  f1o00  6846  fo00  6847  brprcneu  6861  brprcneuALT  6862  dffn5  6929  fsn  7121  funop  7136  funsndifnop  7138  fnsnbOLD  7154  eufnfv  7217  f1ounsn  7260  f1eqcocnv  7289  nfriotadw  7365  nfriotad  7368  riotaprop  7384  oprabidw  7431  oprabid  7432  elrnmpo  7536  ov6g  7564  ovelrn  7576  caovmo  7637  offn  7677  caofinvl  7696  fr3nr  7759  onprc  7765  ordeleqon  7769  onint0  7778  0elsuc  7819  onuninsuci  7824  orduninsuc  7827  ordzsl  7829  onzsl  7830  tfinds  7844  limomss  7855  limom  7866  peano5  7878  xpexr  7903  eqop2  8017  opreuopreu  8019  1stconst  8083  2ndconst  8084  frxp2  8128  frxp3  8135  funsssuppss  8174  dftpos3  8228  dftpos4  8229  oawordeulem  8527  omwordi  8544  nnmwordi  8609  riiner  8776  ecopover  8807  map0g  8870  mapsnd  8872  elixpsn  8923  en0  9003  en0ALT  9004  en0r  9005  en1  9009  snfi  9028  fiprc  9029  sbthlem2  9064  sbthlem4  9066  sbthlem5  9067  0domg  9080  findcard  9136  findcard2  9137  nneneq  9178  sdom1  9198  1sdom2dom  9202  fineqvlem  9214  nfielex  9222  enp1i  9227  elfiun  9378  marypha1lem  9381  oicl  9479  oif  9480  oion  9486  hartogslem1  9492  hartogs  9494  wemapso2  9503  card2on  9504  0wdom  9520  brwdom2  9523  elirrv  9547  inf3lem6  9590  cantnflem3  9648  cantnflem4  9649  wemapwe  9654  cnfcom  9657  ssttrcl  9672  ttrclselem2  9683  tctr  9695  r1tr  9736  r1rankidb  9764  r1pw  9805  scottex  9847  scott0  9848  bnd2  9867  eldju2ndl  9898  tskwe  9924  oncard  9934  cardlim  9946  harsdom  9969  en2eleq  9980  dfac8alem  10001  cardaleph  10061  iunfictbso  10086  infmap2  10188  ackbij1lem18  10207  cff  10219  cfsuc  10229  cff1  10230  cflim2  10235  cfss  10237  sdom2en01  10274  infpssrlem4  10278  fin23lem7  10288  fin23lem11  10289  isfin2-2  10291  fin23lem26  10297  fin23lem19  10308  fin23lem17  10310  isf34lem2  10345  isf34lem4  10349  fin1a2lem6  10377  fin1a2lem10  10381  fin1a2lem12  10383  itunifn  10389  hsmexlem1  10398  axcc2lem  10408  dcomex  10419  axdc3lem4  10425  ondomon  10535  konigthlem  10541  pwcfsdom  10556  cfpwsdom  10557  axpowndlem3  10572  canth4  10620  canthnumlem  10621  canthwelem  10623  canthwe  10624  canthp1lem2  10626  pwfseqlem4  10635  pwfseqlem5  10636  gchaleph  10644  gch2  10648  winainflem  10666  0tsk  10728  rankcf  10750  tskcard  10754  gruina  10791  grutsk  10795  tskmid  10813  indpi  10880  nqereu  10902  mulcanenq  10933  recmulnq  10937  archnq  10953  ltsopr  11005  1ne0sr  11069  0idsr  11070  00sr  11072  leid  11294  lelttric  11305  divcan3  11886  divid  11891  div0  11893  lemul1a  12060  nn1suc  12246  nn0n0n1ge2b  12564  xnn0xr  12573  xnn0nemnf  12579  nn0lt10b  12649  nn0ind-raph  12687  elnn1uz2  12940  indstr2  12942  uzsupss  12955  rpnnen1lem4  12995  rpnnen1lem5  12996  xrnemnf  13133  xrnepnf  13134  mnfltxr  13143  xnn0n0n1ge2b  13148  xnn0ge0  13150  xrlttri  13155  xrlttr  13156  xrleid  13167  qbtwnxr  13217  xmullem2  13282  xlemul1a  13305  xrub  13329  reltxrnmnf  13360  ixxun  13379  xnn0xrge0  13524  fztpval  13605  fseq1p1m1  13617  elfznelfzob  13794  ltweuz  13988  fzfi  13999  fsuppmapnn0fiubex  14019  ser0f  14082  0exp  14124  faclbnd4lem1  14320  bcn1  14340  hashnemnf  14371  hashv01gt1  14372  hashsnle1  14444  hashgt12el2  14450  hashpw  14463  hashf1  14484  fz1isolem  14488  hash2prb  14499  hash3tpb  14522  0wrd0  14567  wrdlen1  14581  ccatvalfn  14608  eqs1  14640  wrdl1exs1  14641  swrdlen  14675  swrdwrdsymb  14690  swrdspsleq  14693  cats1un  14748  wrdind  14749  wrd2ind  14750  swrdccatin1  14752  repswsymballbi  14807  cshw1  14849  scshwfzeqfzo  14853  wrdl2exs2  14973  trclfvcotr  15036  relexp1g  15053  relexp0rel  15064  relexprelg  15065  relexpreld  15067  sgnmulsgn  15136  sqrt0  15282  sqrtsq  15310  mptfzshft  15819  prodf1f  15936  egt2lt3  16252  0dvds  16324  nn0onn  16428  nn0o  16431  divalgmod  16454  flodddiv4  16463  bitsp1o  16481  gcddvds  16551  bezout  16591  lcmdvds  16656  rpdvds  16708  1nprm  16727  prmind2  16733  dvdszzq  16770  nnoddn2prmb  16863  pcpre1  16892  vdwapf  17022  vdwapid1  17025  ram0  17072  ramz  17075  prmolefac  17096  cshws0  17151  prmlem0  17155  strle1  17208  restsspw  17474  prdsdsfn  17508  imasdsfn  17558  imasaddfnlem  17572  imasvscafn  17581  xpsfrnel  17606  isacs1i  17703  cidfn  17725  fnhomeqhomf  17737  comffn  17751  isoval  17812  sscres  17870  cofucl  17935  idffth  17982  ressffth  17987  cat1lem  18143  catcoppccl  18164  estrchomfn  18181  funcestrcsetclem4  18189  funcestrcsetclem7  18192  equivestrcsetc  18198  funcsetcestrclem4  18204  funcsetcestrclem7  18207  1stfcl  18243  2ndfcl  18244  prfcl  18249  evlfcl  18268  curf1cl  18274  curfcl  18278  hofcl  18305  yonedainv  18327  pospo  18389  lubfun  18396  glbfun  18409  joindmss  18423  meetdmss  18437  ipopos  18582  acsficl2d  18598  dirref  18647  mgmidcl  18714  mgmlrid  18715  ielefmnd  18936  smndex1basss  18957  smndex1n0mnd  18964  cntzssv  19389  idresperm  19447  symgvalstruct  19458  pmtrfmvdn0  19523  symggen  19531  psgnunilem1  19554  psgnprfval  19582  slwpgp  19674  frgpmhm  19826  frgpuptinv  19832  frgpup3lem  19838  gsumzoppg  20005  gsumcom2  20036  c0snmhm  20536  srhmsubc  20756  rhmsubclem1  20761  rrgsupp  20777  abv0  20895  zrhrhm  21621  psgnodpmr  21700  frlmphllem  21890  ellspd  21912  psrvscafval  22058  psrridm  22072  ltbwe  22155  psrbag0  22173  psrbagsn  22174  subrgascl  22177  psdmul  22289  mattpostpos  22572  mavmul0  22670  mavmul0g  22671  mdet0f1o  22711  m1detdiag  22715  m2detleiblem5  22743  m2detleiblem6  22744  m2detleiblem3  22747  m2detleiblem4  22748  maducoeval2  22758  d1mat2pmat  22857  chpmat1dlem  22953  chpmat1d  22954  baspartn  23072  eltg3  23080  topnex  23114  fctop  23122  cctop  23124  discld  23207  mretopd  23210  neipeltop  23247  neitr  23298  restcls  23299  ordtbaslem  23306  ordtuni  23308  idcn  23375  cnrmi  23478  cmpsublem  23517  cmpsub  23518  tgcmp  23519  uncmp  23521  hauscmplem  23524  cmpfi  23526  bwth  23528  1stcrestlem  23570  disllycmp  23616  dis1stc  23617  refref  23631  kgeni  23655  1stckgenlem  23671  kqffn  23843  snfil  23982  filconn  24001  cfinfil  24011  ufileu  24037  filufint  24038  fixufil  24040  cfinufil  24046  ufilen  24048  fin1aufil  24050  fmf  24063  rnelfm  24071  flimclslem  24102  hauspwpwf1  24105  supnfcls  24138  flimfnfcls  24146  fclscmp  24148  alexsubALTlem2  24166  alexsubALTlem3  24167  alexsubALT  24169  ptcmplem1  24170  cnextrel  24181  tsmsfbas  24246  ustref  24337  trust  24347  restutop  24355  isusp  24379  xmet0  24460  imasdsf1olem  24491  blfvalps  24501  blfps  24524  blf  24525  restmetu  24688  dscmet  24690  isngp2  24715  nm0  24747  nrginvrcn  24810  nmoix  24847  qdensere  24887  iccconn  24949  iccpnfcnv  25064  xrhmeo  25066  lebnumlem3  25083  metsscmetcld  25435  bcthlem5  25448  csschl  25496  rrxmfval  25526  minveclem3b  25548  cniccbdd  25581  ovolicc2lem4  25640  iunmbl  25673  ioorinv  25696  ioorcl  25697  i1f1lem  25809  limcvallem  25991  ellimc2  25997  limccnp  26011  limccnp2  26012  limcco  26013  perfdvf  26023  recnprss  26024  fncpn  26053  dvcmulf  26065  c1lip1  26117  lhop2  26135  q1pcl  26275  r1pdeglt  26278  ply1remlem  26283  plyssc  26318  ulm0  26512  cxpeq0  26801  cxplea  26819  cxplogb  26909  asinlem  26991  isppw2  27237  muval2  27256  dchrfi  27377  dchrpt  27389  bposlem6  27411  lgsdir2lem2  27448  lgsqr  27473  gausslemma2dlem4  27491  2lgslem2  27517  2lgslem3  27526  2lgs  27529  2sqlem7  27546  2sqlem11  27551  chtppilim  27597  nosgnn0i  27781  nolesgn2ores  27794  nogesgn1ores  27796  nosepnelem  27801  nosepdmlem  27805  nosupbnd1lem3  27832  nosupbnd1lem5  27834  nosupbnd2lem1  27837  noinfbnd1lem3  27847  noinfbnd1lem5  27849  noinfbnd2lem1  27852  oldval  27985  made0  28014  lrrecpo  28092  pncan2s  28225  divscan3d  28387  abssor  28397  om2noseqfo  28449  noseqrdglem  28456  noseqrdgfn  28457  noseqrdg0  28458  onsfi  28507  nohalf  28575  expsne0  28587  pw2divscan3d  28592  tgldimor  28729  tgcgr4  28758  tglnfn  28774  tglnunirn  28775  mirne  28898  mircinv  28899  perpln1  28941  perpln2  28942  tgplnfn  29005  lmiisolem  29048  xmstrkgc  29144  axcgrtr  29174  axsegconlem9  29184  axlowdimlem5  29205  axlowdimlem17  29217  axlowdim1  29218  uhgr0e  29330  edglnl  29402  uhgr0edgfi  29499  issubgr2  29531  subgrprop2  29533  egrsubgr  29536  0grsubgr  29537  0uhgrsubgr  29538  uhgrsubgrself  29539  nbgr1vtx  29617  nbgrssovtx  29620  nb3grprlem1  29639  uvtx01vtx  29656  cplgr1vlem  29688  cplgr1v  29689  usgrexilem  29699  wlkcomp  29889  wlk1walk  29897  wlkp1lem5  29934  uhgrwkspthlem1  30011  pthdlem1  30024  clwlkcomp  30037  lfgrn1cycl  30063  uspgrn2crct  30066  wwlksn0s  30119  usgrwwlks2on  30216  umgrwwlks2on  30217  clwwlkn  30286  clwwlkn1  30301  0ewlk  30374  1ewlk  30375  0spth  30386  upgr1wlkdlem2  30406  wlk2v2e  30417  upgr3v3e3cycl  30440  upgr4cycl4dv4e  30445  eupth0  30474  frgr0v  30522  frgr1v  30531  1vwmgr  30536  ex-opab  30692  grpoinvf  30793  nvmid  30920  nmlnoubi  31057  hiidrcl  31356  hsn0elch  31509  shjshseli  31754  cmbr4i  31862  dfiop2  32014  kbpj  32217  nmopun  32275  adjeq0  32352  kbass2  32378  pjssdif1i  32436  pjinvari  32452  pjcmul2i  32463  pj3i  32469  stge1i  32499  stle0i  32500  sumdmdlem2  32680  dmdbr6ati  32684  dmdbr7ati  32685  rabsnel  32756  unidifsnel  32791  unidifsnne  32792  disjdifprg  32830  ofoprabco  32921  padct  32975  fpwrelmapffslem  32989  nn0mnfxrd  33008  xrlelttric  33009  xnn0gt0  33026  iundisj2cnt  33056  f1ocnt  33057  fz1nnct  33058  fz1nntr  33059  hashxpe  33064  nn0min  33078  sgnmulsgp  33089  wrdt2ind  33186  xrge0tsmsbi  33307  opprabs  33681  rtelextdg2lem  34033  2sqr3minply  34087  locfinref  34148  dispcmp  34166  zartopn  34182  zarcmplem  34188  pstmxmet  34204  xrge0iifcnv  34240  xrge0iif1  34245  qqhre  34327  esumcl  34337  esumpr2  34374  esumpinfval  34380  esumpcvgval  34385  ofcfn  34407  pwsiga  34437  prsiga  34438  sigainb  34443  ldgenpisyslem1  34470  measiuns  34524  relfae  34554  pmeasmono  34631  sitgf  34654  eulerpartgbij  34679  signswch  34865  signslema  34866  signstlen  34871  signstfvn  34873  circlevma  34946  bnj216  35038  bnj151  35182  bnj517  35190  bnj970  35252  bnj1145  35298  bnj1498  35366  r1omhfb  35420  fineqvrep  35422  fineqvac  35424  fineqvnttrclselem1  35429  fineqvnttrclselem2  35430  fineqvnttrclse  35432  fineqvinfep  35433  r1omhfbregs  35445  wevgblacfn  35466  vonf1osev  35467  0nn0m1nnn0  35475  pthhashvtx  35491  acycgr0v  35511  prclisacycgr  35514  umgracycusgr  35517  cusgracyclt3v  35519  subfacp1lem5  35547  erdszelem8  35561  kur14lem1  35569  indispconn  35597  cvmsss2  35637  satfvsuclem2  35723  satfrel  35730  satfrnmapom  35733  satfv0fun  35734  satf00  35737  satf0suclem  35738  fmlasuc0  35747  msubrn  35892  dfon2lem7  36150  brbigcup  36259  elsingles  36279  fnimage  36290  funpartlem  36305  dfrdg4  36314  imagesset  36316  altopthsn  36324  elaltxp  36338  ellines  36515  linethru  36516  rankeq1o  36534  elhf2  36538  hfninf  36549  nn0prpwlem  36695  fneref  36723  neibastop2lem  36733  limsucncmpi  36818  tz9.1tco  36856  bj-exlimmpbir  37411  curryset  37443  bj-snglex  37470  bj-axnul  37569  bj-restpw  37594  bj-inftyexpidisj  37714  topdifinffinlem  37853  relowlssretop  37869  rdgeqoa  37876  finxpreclem6  37902  fvineqsneq  37918  pibt2  37923  poimirlem23  38154  poimirlem29  38160  poimirlem31  38162  volsupnfl  38176  cnambfre  38179  dvasin  38215  dvacos  38216  sdclem2  38253  sstotbnd2  38285  ssbnd  38299  ismgmOLD  38361  grpokerinj  38404  rngomndo  38446  isdrngo1  38467  ac6s6  38683  iss2  38855  relecxrn  38918  sucmapsuc  39000  cosselrels  39086  cnvelrels  39087  brssrid  39093  brcnvssrid  39098  dfdisjs5  39308  eldisjs5  39334  eldisjsim3  39448  mpets2  39466  pets  39477  prtlem12  39503  riotasv2d  39593  lkrscss  39734  islshpkrN  39756  isline  40375  ispointN  40378  0psubN  40385  linepsubN  40388  atpsubN  40389  cdlemk36  41549  diafn  41670  dibfna  41790  dibvalrel  41799  dicvalrelN  41821  diclspsn  41830  dihvalrel  41915  dih1  41922  lclkrlem1  42142  lclkr  42169  mapd1o  42284  mapdin  42298  hdmapfnN  42465  hgmapfnN  42524  lcmineqlem10  42667  sticksstones9  42783  sn-iotalem  42852  readvrec2  42982  readvrec  42983  repncan2  43003  elrfirn  43288  ismrcd1  43291  istopclsd  43293  rabren3dioph  43404  jm2.17b  43550  jm2.22  43584  jm2.23  43585  ttac  43625  pw2f1ocnv  43626  dnnumch1  43633  hbtlem5  43717  mncn0  43728  aaitgo  43751  rngunsnply  43758  unielss  43807  onexlimgt  43832  cantnfresb  43913  dflim5  43918  naddwordnexlem4  43990  safesnsupfiss  44003  safesnsupfidom1o  44005  safesnsupfilb  44006  ensucne0OLD  44118  clcnvlem  44211  relexp01min  44301  ntrf  44711  ssrecnpr  44882  seff  44883  sblpnf  44884  nzss  44891  dvconstbi  44908  ipo0  45022  ifr0  45023  addrfn  45045  subrfn  45046  mulvfn  45047  wfaxrep  45568  refsum2cnlem1  45615  rn1st  45846  ellimciota  46188  dvmptconst  46487  dvmptidg  46489  dvmulcncf  46497  dvdivcncf  46499  stoweidlem26  46598  stoweidlem50  46622  stoweidlem57  46629  aiotaval  47687  ndfatafv2nrn  47813  afv2ndefb  47816  funop1  47875  fun2dmnopgexmpl  47876  2ffzoeq  47920  2ltceilhalf  47924  m1modne  47946  iccpartiltu  48026  iccpartigtl  48027  zofldiv2ALTV  48282  evenprm2  48334  9fppr8  48357  stgoldbwt  48396  nnsum3primesle9  48414  nnsum4primeseven  48420  nnsum4primesevenALTV  48421  tgblthelfgott  48435  dfclnbgr6  48476  cycl3grtri  48567  grtrimap  48568  stgredgel  48577  stgr1  48581  isubgr3stgrlem2  48587  isubgr3stgrlem3  48588  usgrexmpl2trifr  48657  gpg5nbgrvtx13starlem1  48691  gpg5nbgrvtx13starlem2  48692  gpg5nbgrvtx13starlem3  48693  gpg5nbgr3star  48701  gpg3kgrtriex  48709  uspgrex  48770  0mgm  48786  nnsgrpmgm  48796  rngchomffvalALTV  48898  rhmsubcALTVlem1  48901  funcringcsetcALTV2lem4  48913  funcringcsetclem4ALTV  48936  srhmsubcALTV  48945  mapsnop  48975  zlmodzxzldeplem4  49134  zofldiv2  49162  fdivval  49170  nnlog2ge0lt1  49197  dig1  49239  itcoval2  49295  itcoval3  49296  mosn  49442  mo0  49443  mof02  49468  mofeu  49477  f102g  49481  f1mo  49482  tposres0  49506  f1omo  49522  f1omoOLD  49523  resipos  49604  intubeu  49613  unilbeu  49614  sectfn  49658  nelsubclem  49696  idfu1stf1o  49728  imaidfu  49739  oppfvallem  49764  funcoppc3  49776  idfth  49787  idsubc  49789  uptposlem  49826  swapf2fn  49897  swapf1f1o  49904  swapf2f1o  49905  swapf2f1oaALT  49907  fucof1  49951  fucofn2  49953  fucofn22  49969  reldmprcof1  50010  reldmprcof2  50011  fucoppcid  50037  fucoppc  50039  functhinclem1  50073  fullthinc  50079  thincciso  50082  indcthing  50089  indthinc  50091  indthincALT  50092  functermc  50137  discsntermlem  50199  reldmlan2  50246  reldmran2  50247  rellan  50252  relran  50253  termolmd  50299