Theorem mpbir 230

Description: An inference from a biconditional, related to modus ponens. (Contributed by NM, 28-Dec-1992.)

Hypotheses

Ref	Expression
mpbir.min	⊢ 𝜓
mpbir.maj	⊢ (𝜑 ↔ 𝜓)

Assertion

Ref	Expression
mpbir	⊢ 𝜑

Proof of Theorem mpbir

Step	Hyp	Ref	Expression
1		mpbir.min	. 2 ⊢ 𝜓
2		mpbir.maj	. . 3 ⊢ (𝜑 ↔ 𝜓)
3	2	biimpri 227	. 2 ⊢ (𝜓 → 𝜑)
4	1, 3	ax-mp 5	1 ⊢ 𝜑

Syntax hints:   ↔ 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:  pm5.74ri  271  con4bii  320  imnani  400  mpbir2an  707  imorri  851  orri  858  mpbir3an  1339  xorexmid  1521  tru  1543  had1  1606  nic-mpALT  1676  nic-ax  1677  nic-axALT  1678  nfi  1792  mpgbir  1803  nfxfr  1856  19.35ri  1883  ax5e  1916  ax6ev  1974  sbt  2070  equsb1v  2105  ax13  2375  ax13ALT  2425  moanmo  2624  axi12  2707  axbnd  2708  axexte  2710  axextmo  2713  nulmo  2714  vexw  2721  eqeltri  2835  nfcxfr  2904  neir  2945  neirr  2951  eqnetri  3013  nelir  3051  mprgbir  3078  cbvrexdva2  3382  issetri  3438  moeq  3637  rmoeq  3668  cdeqi  3695  eqsstri  3951  3sstr4i  3960  rmo0  4290  rabnc  4318  reuprg  4636  tpid1  4701  tpid2  4703  mosneq  4770  pwv  4833  uni0  4866  int0  4890  eqbrtri  5091  tr0  5198  trv  5199  zfrep4  5215  axnulALT  5223  0ex  5226  inex1  5236  elpwi2  5265  elpwi2OLD  5266  0elpw  5273  axpow2  5285  axpow3  5286  dvdemo1  5291  vpwex  5295  zfpair2  5348  exss  5372  brv  5381  opwo0id  5405  moop2  5410  pwundifOLD  5477  0sn0ep  5490  po0  5511  epse  5563  relxp  5598  rel0  5698  relopabiv  5719  relopabi  5721  relopabiALT  5722  eliunxp  5735  opeliunxp2  5736  dmi  5819  dmep  5821  domepOLD  5822  xpidtr  6016  xpima  6074  dmsn0  6101  cnvsn0  6102  0elon  6304  funmpt  6456  funmpt2  6457  funcnv0  6484  isarep2  6507  fresaunres2  6630  f0  6639  f10d  6733  f1o00  6734  f1oi  6737  f1osn  6739  brprcneu  6747  fvprc  6748  opabiotafun  6831  fvopab3ig  6853  opabex  7078  mptexgf  7080  eufnfv  7087  isof1oopb  7176  ncanth  7210  mpofun  7376  mpofunOLD  7377  reldmmpo  7386  ovid  7392  ovidig  7393  ovidi  7394  ovig  7397  ov3  7413  caovmo  7487  relmptopab  7497  porpss  7558  uniex2  7569  tfinds2  7685  finds  7719  finds2  7721  oprabex  7792  oprabex3  7793  f1stres  7828  f2ndres  7829  relmpoopab  7905  fsplitfpar  7930  opeliunxp2f  7997  tpos0  8043  wfrrelOLD  8116  wfrlem14OLD  8124  wfrlem16OLD  8126  issmo  8150  tfrlem6  8184  tfrlem8  8186  tfrlem16  8195  tfr1a  8196  tfr1  8199  tz7.44lem1  8207  seqomlem2  8252  seqomlem3  8253  seqomlem4  8254  fnseqom  8256  0lt1o  8296  0we1  8298  eqer  8491  ecopover  8568  mapsnf1o3  8641  ssdomg  8741  en0  8758  en0OLD  8759  ensn1  8761  ensn1OLD  8762  snfi  8788  enrefnn  8791  xpcomf1o  8801  map2xp  8883  limensuci  8889  sdom1  8952  unblem4  8999  fidomdm  9026  marypha1lem  9122  hartogslem1  9231  hartogs  9233  card2on  9243  nelaneq  9288  epinid0  9289  ruALT  9292  elnanel  9295  cnvepnep  9296  inf2  9311  inf3lem6  9321  infeq5i  9324  zfinf2  9330  cantnflt  9360  cnfcom  9388  trcl  9417  tz9.1c  9419  tc2  9431  r1funlim  9455  r1fnon  9456  karden  9584  tskwe  9639  cardprclem  9668  pm54.43  9690  r0weon  9699  iunmapdisj  9710  alephfnon  9752  alephfplem4  9794  alephfp  9795  alephval3  9797  kmlem2  9838  dju1dif  9859  ackbij1  9925  ackbij2lem2  9927  ackbij2  9930  infpssrlem3  9992  hsmexlem4  10116  hsmexlem5  10117  ac2  10148  axac3  10151  ac6  10167  axdclem2  10207  dmct  10211  ondomon  10250  alephsucpw  10257  pwcfsdom  10270  cfpwsdom  10271  smobeth  10273  axpowndlem3  10286  zfcndun  10302  zfcndpow  10303  zfcndinf  10305  zfcndac  10306  wunex2  10425  uniwun  10427  wuncval2  10434  grur1  10507  axgroth5  10511  axgroth2  10512  axgroth6  10515  axgroth3  10518  grothtsk  10522  inaprc  10523  ltsopi  10575  dmaddpi  10577  dmmulpi  10578  1lt2pi  10592  nqerf  10617  addnqf  10635  mulnqf  10636  1lt2nq  10660  m1p1sr  10779  m1m1sr  10780  0lt1sr  10782  axaddf  10832  axmulf  10833  ax1cn  10836  subaddrii  11240  ixi  11534  recgt0ii  11811  nn1suc  11925  neg1lt0  12020  4d2e2  12073  arch  12160  un0mulcl  12197  pnf0xnn0  12242  3halfnz  12329  nummac  12411  indstr  12585  mnfltpnf  12791  ioof  13108  0nelfz1  13204  fzp1disj  13244  fzp1nel  13269  fzof  13313  om2uzrani  13600  om2uzf1oi  13601  uzrdglem  13605  uzrdgfni  13606  uzrdg0i  13607  ltwenn  13610  hashgf1o  13619  axdc4uzlem  13631  sq0  13837  irec  13846  facmapnn  13927  hashkf  13974  hashfxnn0  13979  hashf  13980  hash0  14010  prhash2ex  14042  hashsslei  14069  hashxplem  14076  hashbclem  14092  hashf1lem1  14096  hashf1lem1OLD  14097  s1dm  14241  eqs1  14245  ccat2s1p1  14264  cats1un  14362  revs1  14406  0csh0  14434  cshw1  14463  cats1fvn  14499  funcnvs1  14553  pfx2  14588  relexp0g  14661  relexpsucnnr  14664  rtrclreclem1  14696  dfrtrclrec2  14697  rtrclreclem2  14698  rtrclreclem4  14700  dfrtrcl2  14701  climmo  15194  fsumcom2  15414  ackbijnn  15468  incexclem  15476  infcvgaux1i  15497  fprodcom2  15622  bpolylem  15686  bpoly3  15696  bpoly4  15697  efcvgfsum  15723  cos1bnd  15824  cos2bnd  15825  znnen  15849  qnnen  15850  aleph1re  15882  3dvds  15968  n2dvdsm1  16006  divalglem5  16034  flodddiv4  16050  sadcaddlem  16092  sadadd2lem  16094  sadadd3  16096  sadaddlem  16101  lcmf0  16267  lcmfunsnlem2lem1  16271  lcmfunsnlem2  16273  coprmprod  16294  coprmproddvdslem  16295  2prm  16325  3lcm2e6  16364  phicl2  16397  pockthi  16536  unbenlem  16537  prmrec  16551  vdwlem13  16622  vdwnn  16627  ramcl2  16645  prmgapprmo  16691  mod2xnegi  16700  modsubi  16701  structcnvcnv  16782  strleun  16786  setsres  16807  strfv  16833  starvndxnbasendx  16940  starvndxnplusgndx  16941  starvndxnmulrndx  16942  scandxnbasendx  16952  scandxnplusgndx  16953  scandxnmulrndx  16954  vscandxnbasendx  16957  vscandxnplusgndx  16958  vscandxnmulrndx  16959  vscandxnscandx  16960  ipndxnbasendx  16968  ipndxnplusgndx  16969  ipndxnmulrndx  16970  tsetndxnplusgndx  16992  tsetndxnmulrndx  16993  slotstnscsi  16994  plendxnplusgndx  17005  plendxnmulrndx  17006  plendxnscandx  17007  plendxnvscandx  17008  dsndxnplusgndx  17021  dsndxnmulrndx  17022  slotsdnscsi  17023  dsndxntsetndx  17024  unifndxntsetndx  17030  0rest  17057  firest  17060  restid  17061  prdsval  17083  prdsbas  17085  prdsplusg  17086  prdsmulr  17087  prdsvsca  17088  imasaddfnlem  17156  imasvscafn  17165  oppchomfvalOLD  17341  oppcbasOLD  17346  2oppchomf  17352  rescbasOLD  17459  resccoOLD  17463  rescabs  17464  0ssc  17468  0subcat  17469  idfucl  17512  homarel  17667  dmaf  17680  cdaf  17681  setc2ohom  17726  catcfuccl  17750  catcfucclOLD  17751  relxpchom  17814  catcxpccl  17840  catcxpcclOLD  17841  oppchofcl  17894  oyoncl  17904  odubas  17925  letsr  18226  mgmidmo  18259  efmndmgm  18439  smndex1ibas  18454  smndex1mgm  18461  smndex1mnd  18464  smndex2dbas  18468  smndex2dnrinv  18469  smndex2hbas  18470  pwmnd  18491  releqg  18718  ga0  18819  oppglemOLD  18870  psgnunilem3  19019  psgnunilem4  19020  pmtrsn  19042  efgval  19238  efger  19239  efgsval2  19254  efgsp1  19258  efgsfo  19260  efgredleme  19264  efgredlem  19268  efgred  19269  cygctb  19408  gsum2d2lem  19489  gsum2d2  19490  gsumcom2  19491  dprd2d2  19562  pgpfaclem1  19599  mgplemOLD  19640  mgpressOLD  19651  opprlemOLD  19783  reldvdsr  19801  00lsp  20158  sralemOLD  20355  srasca  20362  sravsca  20363  cnfldfun  20522  cnfldfunALT  20523  xrsmgm  20545  znbaslemOLD  20655  resubdrg  20725  ocv0  20794  cssval  20799  thlbas  20813  thlle  20814  islinds2  20930  psrvscafval  21069  opsrbaslemOLD  21161  psrbag0  21180  00ply1bas  21321  ply1plusgfvi  21323  matsca  21472  m2detleib  21688  tgdom  22036  tgidm  22038  indistps2ALT  22073  restbas  22217  resttopon  22220  rest0  22228  leordtval2  22271  iocpnfordt  22274  icomnfordt  22275  iooordt  22276  ist1-3  22408  1stcfb  22504  comppfsc  22591  1stckgen  22613  ptbasfi  22640  dfac14  22677  opnfbas  22901  hauspwpwf1  23046  alexsubALT  23110  ptcmplem5  23115  cnextrel  23122  ust0  23279  tuslemOLD  23327  0met  23427  prdsdsf  23428  prdsxmetlem  23429  prdsmet  23431  setsmsbas  23536  setsmsds  23537  prdsbl  23553  tngdsOLD  23718  qtopbaslem  23828  xrtgioo  23875  xrsdsre  23879  zcld  23882  recld2  23883  reperflem  23887  retopconn  23898  iccpnfcnv  24013  bndth  24027  nmoleub2lem2  24185  zclmncvs  24217  recmet  24392  resscdrg  24427  ishl2  24439  recms  24449  volf  24598  iundisj2  24618  volsup  24625  icombl  24633  ioombl  24634  ismbf3d  24723  0plef  24741  0pledm  24742  itg1ge0  24755  mbfi1fseqlem5  24789  itg2addlem  24828  reldv  24939  limciun  24963  dvexp  25022  dveflem  25048  lhop1lem  25082  lhop  25085  elply2  25262  elplyd  25268  ply1term  25270  ply0  25274  plymullem  25282  qaa  25388  pserulm  25486  pserdvlem2  25492  efcn  25507  sincosq1lem  25559  tangtx  25567  sincos4thpi  25575  pigt3  25579  pige3ALT  25581  efif1olem4  25606  logf1o  25625  relogf1o  25627  log1  25646  loge  25647  relogiso  25658  dvrelog  25697  relogcn  25698  logcn  25707  cxpcn3  25806  resqrtcn  25807  2logb9irr  25850  leibpi  25997  log2ublem1  26001  birthday  26009  emcllem5  26054  harmonicbnd  26058  harmonicbnd2  26059  harmonicbnd3  26062  lgamgulm2  26090  lgamcvglem  26094  gamf  26097  ppiltx  26231  ppiublem1  26255  ppiub  26257  bclbnd  26333  bpos1lem  26335  bposlem8  26344  lgsquadlem2  26434  2sqlem9  26480  2sqlem10  26481  addsqnreup  26496  chebbnd1  26525  selberg2lem  26603  pntrsumo1  26618  selbergsb  26628  pntpbnd  26641  istrkg2ld  26725  tgcgr4  26796  ttgval  27140  ttglemOLD  27142  cchhllemOLD  27158  ax5seglem7  27206  axlowdimlem4  27216  axlowdimlem6  27218  axlowdimlem7  27219  axlowdimlem10  27222  axlowdimlem13  27225  axlowdimlem16  27228  uhgr0e  27344  uhgr0  27346  upgrbi  27366  umgrbi  27374  usgr0  27513  lfuhgr1v0e  27524  usgrexmpllem  27530  usgrexmpl  27533  griedg0prc  27534  cplgr0  27695  usgrexilem  27710  cffldtocusgr  27717  rgrusgrprc  27859  rusgrprc  27860  rgrprcx  27862  rgrx0ndm  27863  usgr2pthlem  28032  pthdlem2  28037  uspgrn2crct  28074  wwlksnext  28159  wwlksnfi  28172  disjxwwlkn  28179  clwwlknondisj  28376  0ewlk  28379  0wlk  28381  0pth  28390  1pthdlem1  28400  1trld  28407  wlk2v2elem2  28421  wlk2v2e  28422  upgr3v3e3cycl  28445  upgr4cycl4dv4e  28450  dfconngr1  28453  0conngr  28457  konigsbergumgr  28516  2wspmdisj  28602  2clwwlk2clwwlk  28615  numclwwlk3lem2lem  28648  numclwwlk3lem2  28649  ex-dif  28688  ex-in  28690  ex-eprel  28698  ex-id  28699  ex-fl  28712  ex-mod  28714  ex-hash  28718  ex-fpar  28727  avril1  28728  2bornot2b  28729  0vfval  28869  vsfval  28896  ajmoi  29121  ajfuni  29122  normlem2  29374  norm3adifii  29411  hhip  29440  hlim0  29498  hlimcaui  29499  hlimf  29500  hhssnv  29527  shscli  29580  shsval2i  29650  h1de2i  29816  fh3i  29886  fh4i  29887  cm2mi  29889  qlaxr3i  29899  mayetes3i  29992  ho0f  30014  hoif  30017  hodidi  30050  ho0subi  30058  hosd1i  30085  adjmo  30095  nmopsetn0  30128  nmfnsetn0  30141  funadj  30149  funcnvadj  30156  nmcexi  30289  cnlnadjlem8  30337  nmoptri2i  30362  opsqrlem4  30406  hmopidmchi  30414  pjoci  30443  pjinvari  30454  abrexdomjm  30753  elim2ifim  30789  iundisj2f  30830  rinvf1o  30866  dfcnv2  30915  snct  30950  fzodif2  31015  iundisj2fi  31020  dp2lt10  31060  dp2ltc  31063  dplti  31081  dpgti  31082  dpexpp1  31084  gsumle  31252  xrge0slmod  31450  zarcls  31726  zartopn  31727  xrge0pluscn  31792  zlmds  31814  zlmtset  31815  qqhre  31870  esumrnmpt2  31936  esumfsup  31938  esumpcvgval  31946  hasheuni  31953  esumcvg  31954  esumcvgsum  31956  esumsup  31957  esum2d  31961  dmsigagen  32012  ldgenpisyslem3  32033  measvuni  32082  voliune  32097  volfiniune  32098  br2base  32136  dya2iocuni  32150  eulerpartlem1  32234  eulerpartlemt  32238  eulerpartgbij  32239  fib0  32266  coinfliprv  32349  ballotlem2  32355  ballotlemic  32373  ballotlem7  32402  ballotth  32404  plymul02  32425  rpsqrtcn  32473  chtvalz  32509  circlemethnat  32521  circlevma  32522  circlemethhgt  32523  hgt750lem  32531  bnj226  32613  bnj1101  32664  bnj110  32738  bnj149  32755  bnj150  32756  bnj151  32757  bnj517  32765  bnj580  32793  bnj865  32803  bnj900  32809  bnj996  32836  bnj1110  32862  bnj1133  32869  bnj1128  32870  bnj1145  32873  bnj1137  32875  bnj1171  32880  bnj1176  32885  f1resfz0f1d  32972  subfacp1lem5  33046  subfacp1lem6  33047  kur14lem9  33076  cvmcov2  33137  cvmliftlem1  33147  cvmliftlem4  33150  cvmliftlem5  33151  gonanegoal  33214  satfv0  33220  satfv0fun  33233  fmlan0  33253  gonan0  33254  fmla0disjsuc  33260  ex-sategoelel12  33289  msrfo  33408  problem5  33527  brtpid1  33567  brtpid2  33568  brtpid3  33569  logi  33606  faclimlem1  33615  axextndbi  33686  poseq  33729  sltval2  33786  noxp1o  33793  nosepnelem  33809  noetasuplem2  33864  noetainflem2  33868  0slt1s  33950  txprel  34108  relsset  34117  relbigcup  34126  fvbigcup  34131  fnsingle  34148  fvsingle  34149  snelsingles  34151  funimage  34157  fullfunfnv  34175  imagesset  34182  funtransport  34260  colinrel  34286  funray  34369  funline  34371  0hf  34406  neibastop2lem  34476  filnetlem3  34496  nrmo  34526  waj-ax  34530  lukshef-ax2  34531  arg-ax  34532  limsucncmpi  34561  dnizeq0  34582  knoppcnlem8  34607  knoppcnlem11  34610  cnndvlem1  34644  bj-babylob  34713  bj-ax12ssb  34766  bj-nnfnth  34852  bj-disjcsn  35068  bj-snsetex  35080  bj-0eltag  35095  bj-2upln0  35140  bj-2upln1upl  35141  f1omptsnlem  35434  f1omptsn  35435  icoreresf  35450  relowlssretop  35461  relowlpssretop  35462  domalom  35502  matunitlindf  35702  poimirlem3  35707  poimirlem9  35713  poimirlem16  35720  poimirlem17  35721  poimirlem18  35722  poimirlem19  35723  poimirlem20  35724  poimirlem26  35730  mblfinlem1  35741  mblfinlem2  35742  ismblfin  35745  voliunnfl  35748  cnambfre  35752  abrexdom  35815  fdc  35830  cncfres  35850  heibor1lem  35894  grposnOLD  35967  bicontr  36165  an12i  36183  tsim1  36215  ac6s6f  36258  vvdifopab  36326  brcnvrabga  36404  opabf  36425  xrnrel  36430  relcoels  36474  cnvcosseq  36487  refrelcoss3  36508  refrelcoss2  36509  symrelcoss2  36511  refrelcoss  36567  symrelcoss  36601  n0eldmqs  36688  ax13fromc9  36847  dedths  36903  renegclALT  36904  hlhilslemOLD  39880  12gcd5e1  39939  60gcd7e1  39941  lcmineqlem23  39987  dvrelog2  40000  dvrelog3  40001  dvrelog2b  40002  aks4d1p1p6  40009  aks4d1p1p7  40010  aks4d1p1  40012  sticksstones22  40052  2xp3dxp2ge1d  40090  acos1half  40098  sn-axprlem3  40114  rtprmirr  40268  moxfr  40430  mapfzcons1  40455  diophrw  40497  0dioph  40516  vdioph  40517  rabren3dioph  40553  2nn0ind  40683  rpnnen3  40770  kelac2lem  40805  frlmpwfi  40839  ifpbiidcor2  40988  iscard4  41038  sqrtcval  41138  resqrtvalex  41142  eliunov2  41176  xphe  41278  0he  41279  he0  41281  snhesn  41283  idhe  41284  frege54cor1c  41412  clsk1independent  41545  neicvgnvor  41615  amgm2d  41698  amgm3d  41699  amgm4d  41700  ismnushort  41808  lhe4.4ex1a  41836  rusbcALT  41946  ipo0  41956  ifr0  41957  vk15.4j  42037  2sb5nd  42069  dfvd1ir  42082  dfvd2anir  42093  dfvd2ir  42095  dfvd3ir  42102  dfvd3anir  42105  iden2  42123  e0bir  42286  uun2221p1  42323  uun2221p2  42324  2sb5ndVD  42419  2sb5ndALT  42441  iunconnlem2  42444  fnchoice  42461  unisn0  42491  eliincex  42549  icof  42648  supminfxr  42894  fsumiunss  43006  climlimsupcex  43200  liminfltlimsupex  43212  liminflelimsupcex  43228  xlimrel  43251  xlimfun  43286  resincncf  43306  dvnprodlem3  43379  volioc  43403  volico  43414  dmvolss  43416  volioof  43418  stoweidlem13  43444  stoweidlem34  43465  stirlinglem5  43509  stirlinglem13  43517  stirlingr  43521  fourierdlem42  43580  fourierdlem62  43599  fouriersw  43662  etransc  43714  salexct  43763  salexct2  43768  salgencntex  43772  sge0rnn0  43796  gsumge0cl  43799  sge00  43804  sge0resplit  43834  sge0reuz  43875  omeiunle  43945  0ome  43957  icoresmbl  43971  ovn0lem  43993  ovnhoilem1  44029  hspmbl  44057  ovolval5lem3  44082  nsssmfmbf  44201  mbfpsssmf  44205  smfresal  44209  smfmullem4  44215  smfpimbor1lem1  44219  smfpimbor1lem2  44220  aistia  44279  aisfina  44280  aiffnbandciffatnotciffb  44286  axorbciffatcxorb  44287  abnotbtaxb  44297  abnotataxb  44298  eusnsn  44407  aiotaval  44474  aiota0ndef  44476  fundcmpsurinjimaid  44751  ichv  44789  ichf  44790  ichid  44791  icht  44792  ichcircshi  44794  icheq  44802  spr0nelg  44816  m3prm  44932  m7prm  44940  0noddALTV  45029  2noddALTV  45033  341fppr2  45074  9fppr8  45077  nfermltl8rev  45082  nfermltl2rev  45083  nfermltlrev  45084  sbgoldbo  45127  nnsum3primes4  45128  evengpop3  45138  oddinmgm  45257  nn0mnd  45261  2zrngamgm  45385  2zrngaabl  45390  2zrngmmgm  45392  2zrngnring  45398  fldhmsubc  45530  fldhmsubcALTV  45548  eliunxp2  45557  zlmodzxzldeplem  45727  zlmodzxzldep  45733  ldepslinc  45738  rrx2xpreen  45953  rrx2plordisom  45957  line2ylem  45985  line2  45986  line2x  45988  inlinecirc02plem  46020  mosn  46046  mof0  46053  mof0ALT  46055  f1omo  46076  prstcleval  46237  prstcocval  46239  ex-gte  46317  empty-surprise  46372  eximp-surprise2  46375  amgmw2d  46394