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  321  imnani  401  mpbir2an  708  imorri  852  orri  859  mpbir3an  1340  xorexmid  1524  tru  1543  had1  1605  nic-mpALT  1675  nic-ax  1676  nic-axALT  1677  nfi  1791  mpgbir  1802  nfxfr  1856  19.35ri  1883  ax5e  1916  ax6ev  1974  sbt  2070  equsb1v  2104  ax13  2376  ax13ALT  2426  moanmo  2625  axi12  2708  axbnd  2709  axexte  2711  axextmo  2714  nulmo  2715  vexw  2722  eqeltri  2836  nfcxfr  2906  neir  2947  neirr  2953  eqnetri  3015  nelir  3053  mprgbir  3080  cbvrexdva2  3394  issetri  3449  moeq  3643  rmoeq  3674  cdeqi  3701  eqsstri  3956  3sstr4i  3965  rmo0  4294  rabnc  4322  reuprg  4640  tpid1  4705  tpid2  4707  mosneq  4774  pwv  4837  uni0  4870  int0  4894  eqbrtri  5096  tr0  5203  trv  5204  zfrep4  5221  axnulALT  5229  0ex  5232  inex1  5242  elpwi2  5271  elpwi2OLD  5272  0elpw  5279  axpow2  5291  axpow3  5292  dvdemo1  5297  vpwex  5301  zfpair2  5354  exss  5379  brv  5388  opwo0id  5412  moop2  5417  pwundifOLD  5487  0sn0ep  5500  po0  5521  epse  5573  relxp  5608  rel0  5711  relopabiv  5732  relopabi  5734  relopabiALT  5735  eliunxp  5749  opeliunxp2  5750  dmi  5833  dmep  5835  domepOLD  5836  xpidtr  6032  xpima  6090  dmsn0  6117  cnvsn0  6118  0elon  6323  funmpt  6479  funmpt2  6480  funcnv0  6507  isarep2  6532  fresaunres2  6655  f0  6664  f10d  6759  f1o00  6760  f1oi  6763  f1osn  6765  brprcneu  6773  brprcneuALT  6774  opabiotafun  6858  fvopab3ig  6880  opabex  7105  mptexgf  7107  eufnfv  7114  isof1oopb  7205  ncanth  7239  mpofun  7407  mpofunOLD  7408  reldmmpo  7417  ovid  7423  ovidig  7424  ovidi  7425  ovig  7428  ov3  7444  caovmo  7518  relmptopab  7528  porpss  7589  uniex2  7600  tfinds2  7719  finds  7754  finds2  7756  oprabex  7828  oprabex3  7829  f1stres  7864  f2ndres  7865  relmpoopab  7943  fsplitfpar  7968  opeliunxp2f  8035  tpos0  8081  wfrrelOLD  8154  wfrlem14OLD  8162  wfrlem16OLD  8164  issmo  8188  tfrlem6  8222  tfrlem8  8224  tfrlem16  8233  tfr1a  8234  tfr1  8237  tz7.44lem1  8245  seqomlem2  8291  seqomlem3  8292  seqomlem4  8293  fnseqom  8295  0lt1o  8343  0we1  8345  eqer  8542  ecopover  8619  mapsnf1o3  8692  ssdomg  8795  en0  8812  en0OLD  8813  en0r  8815  ensn1  8816  ensn1OLD  8817  snfi  8843  enrefnn  8846  xpcomf1o  8857  map2xp  8943  limensuci  8949  sdom1  9031  unblem4  9078  fidomdm  9105  marypha1lem  9201  hartogslem1  9310  hartogs  9312  card2on  9322  nelaneq  9367  epinid0  9368  ruALT  9371  elnanel  9374  cnvepnep  9375  inf2  9390  inf3lem6  9400  infeq5i  9403  zfinf2  9409  cantnflt  9439  cnfcom  9467  trcl  9495  tz9.1c  9497  tc2  9509  r1funlim  9533  r1fnon  9534  karden  9662  tskwe  9717  cardprclem  9746  pm54.43  9768  r0weon  9777  iunmapdisj  9788  alephfnon  9830  alephfplem4  9872  alephfp  9873  alephval3  9875  kmlem2  9916  dju1dif  9937  ackbij1  10003  ackbij2lem2  10005  ackbij2  10008  infpssrlem3  10070  hsmexlem4  10194  hsmexlem5  10195  ac2  10226  axac3  10229  ac6  10245  axdclem2  10285  dmct  10289  ondomon  10328  alephsucpw  10335  pwcfsdom  10348  cfpwsdom  10349  smobeth  10351  axpowndlem3  10364  zfcndun  10380  zfcndpow  10381  zfcndinf  10383  zfcndac  10384  wunex2  10503  uniwun  10505  wuncval2  10512  grur1  10585  axgroth5  10589  axgroth2  10590  axgroth6  10593  axgroth3  10596  grothtsk  10600  inaprc  10601  ltsopi  10653  dmaddpi  10655  dmmulpi  10656  1lt2pi  10670  nqerf  10695  addnqf  10713  mulnqf  10714  1lt2nq  10738  m1p1sr  10857  m1m1sr  10858  0lt1sr  10860  axaddf  10910  axmulf  10911  ax1cn  10914  subaddrii  11319  ixi  11613  recgt0ii  11890  nn1suc  12004  neg1lt0  12099  4d2e2  12152  arch  12239  un0mulcl  12276  pnf0xnn0  12321  3halfnz  12408  nummac  12491  indstr  12665  mnfltpnf  12871  ioof  13188  0nelfz1  13284  fzp1disj  13324  fzp1nel  13349  fzof  13393  om2uzrani  13681  om2uzf1oi  13682  uzrdglem  13686  uzrdgfni  13687  uzrdg0i  13688  ltwenn  13691  hashgf1o  13700  axdc4uzlem  13712  sq0  13918  irec  13927  facmapnn  14008  hashkf  14055  hashfxnn0  14060  hashf  14061  hash0  14091  prhash2ex  14123  hashsslei  14150  hashxplem  14157  hashbclem  14173  hashf1lem1  14177  hashf1lem1OLD  14178  s1dm  14322  eqs1  14326  ccat2s1p1  14345  cats1un  14443  revs1  14487  0csh0  14515  cshw1  14544  cats1fvn  14580  funcnvs1  14634  pfx2  14669  relexp0g  14742  relexpsucnnr  14745  rtrclreclem1  14777  dfrtrclrec2  14778  rtrclreclem2  14779  rtrclreclem4  14781  dfrtrcl2  14782  climmo  15275  fsumcom2  15495  ackbijnn  15549  incexclem  15557  infcvgaux1i  15578  fprodcom2  15703  bpolylem  15767  bpoly3  15777  bpoly4  15778  efcvgfsum  15804  cos1bnd  15905  cos2bnd  15906  znnen  15930  qnnen  15931  aleph1re  15963  3dvds  16049  n2dvdsm1  16087  divalglem5  16115  flodddiv4  16131  sadcaddlem  16173  sadadd2lem  16175  sadadd3  16177  sadaddlem  16182  lcmf0  16348  lcmfunsnlem2lem1  16352  lcmfunsnlem2  16354  coprmprod  16375  coprmproddvdslem  16376  2prm  16406  3lcm2e6  16445  phicl2  16478  pockthi  16617  unbenlem  16618  prmrec  16632  vdwlem13  16703  vdwnn  16708  ramcl2  16726  prmgapprmo  16772  mod2xnegi  16781  modsubi  16782  structcnvcnv  16863  strleun  16867  setsres  16888  strfv  16914  starvndxnbasendx  17023  starvndxnplusgndx  17024  starvndxnmulrndx  17025  scandxnbasendx  17035  scandxnplusgndx  17036  scandxnmulrndx  17037  vscandxnbasendx  17040  vscandxnplusgndx  17041  vscandxnmulrndx  17042  vscandxnscandx  17043  ipndxnbasendx  17051  ipndxnplusgndx  17052  ipndxnmulrndx  17053  slotsdifipndx  17054  tsetndxnplusgndx  17076  tsetndxnmulrndx  17077  tsetndxnstarvndx  17078  slotstnscsi  17079  plendxnplusgndx  17090  plendxnmulrndx  17091  plendxnscandx  17092  plendxnvscandx  17093  slotsdifplendx  17094  basendxnocndx  17102  plendxnocndx  17103  dsndxnplusgndx  17109  dsndxnmulrndx  17110  slotsdnscsi  17111  dsndxntsetndx  17112  slotsdifdsndx  17113  unifndxntsetndx  17119  slotsdifunifndx  17120  slotsdifplendx2  17136  slotsdifocndx  17137  0rest  17149  firest  17152  restid  17153  prdsval  17175  prdsbas  17177  prdsplusg  17178  prdsmulr  17179  prdsvsca  17180  imasaddfnlem  17248  imasvscafn  17257  oppchomfvalOLD  17433  oppcbasOLD  17438  2oppchomf  17444  rescbasOLD  17551  resccoOLD  17555  rescabsOLD  17557  0ssc  17561  0subcat  17562  idfucl  17605  homarel  17760  dmaf  17773  cdaf  17774  setc2ohom  17819  catcfuccl  17843  catcfucclOLD  17844  relxpchom  17907  catcxpccl  17933  catcxpcclOLD  17934  oppchofcl  17987  oyoncl  17997  odubasOLD  18019  letsr  18320  mgmidmo  18353  efmndmgm  18533  smndex1ibas  18548  smndex1mgm  18555  smndex1mnd  18558  smndex2dbas  18562  smndex2dnrinv  18563  smndex2hbas  18564  pwmnd  18585  releqg  18812  ga0  18913  oppglemOLD  18964  psgnunilem3  19113  psgnunilem4  19114  pmtrsn  19136  efgval  19332  efger  19333  efgsval2  19348  efgsp1  19352  efgsfo  19354  efgredleme  19358  efgredlem  19362  efgred  19363  cygctb  19502  gsum2d2lem  19583  gsum2d2  19584  gsumcom2  19585  dprd2d2  19656  pgpfaclem1  19693  mgplemOLD  19734  mgpressOLD  19745  opprlemOLD  19877  reldvdsr  19895  00lsp  20252  sralemOLD  20449  srascaOLD  20457  sravscaOLD  20459  cnfldfun  20618  cnfldfunALT  20619  cnfldfunALTOLD  20620  xrsmgm  20642  znbaslemOLD  20752  resubdrg  20822  ocv0  20891  cssval  20896  thlbasOLD  20911  thlleOLD  20913  islinds2  21029  psrvscafval  21168  opsrbaslemOLD  21260  psrbag0  21279  00ply1bas  21420  ply1plusgfvi  21422  matscaOLD  21572  m2detleib  21789  tgdom  22137  tgidm  22139  indistps2ALT  22174  restbas  22318  resttopon  22321  rest0  22329  leordtval2  22372  iocpnfordt  22375  icomnfordt  22376  iooordt  22377  ist1-3  22509  1stcfb  22605  comppfsc  22692  1stckgen  22714  ptbasfi  22741  dfac14  22778  opnfbas  23002  hauspwpwf1  23147  alexsubALT  23211  ptcmplem5  23216  cnextrel  23223  ust0  23380  tuslemOLD  23428  0met  23528  prdsdsf  23529  prdsxmetlem  23530  prdsmet  23532  setsmsbasOLD  23638  setsmsdsOLD  23640  prdsbl  23656  tngdsOLD  23821  qtopbaslem  23931  xrtgioo  23978  xrsdsre  23982  zcld  23985  recld2  23986  reperflem  23990  retopconn  24001  iccpnfcnv  24116  bndth  24130  nmoleub2lem2  24288  zclmncvs  24321  recmet  24496  resscdrg  24531  ishl2  24543  recms  24553  volf  24702  iundisj2  24722  volsup  24729  icombl  24737  ioombl  24738  ismbf3d  24827  0plef  24845  0pledm  24846  itg1ge0  24859  mbfi1fseqlem5  24893  itg2addlem  24932  reldv  25043  limciun  25067  dvexp  25126  dveflem  25152  lhop1lem  25186  lhop  25189  elply2  25366  elplyd  25372  ply1term  25374  ply0  25378  plymullem  25386  qaa  25492  pserulm  25590  pserdvlem2  25596  efcn  25611  sincosq1lem  25663  tangtx  25671  sincos4thpi  25679  pigt3  25683  pige3ALT  25685  efif1olem4  25710  logf1o  25729  relogf1o  25731  log1  25750  loge  25751  relogiso  25762  dvrelog  25801  relogcn  25802  logcn  25811  cxpcn3  25910  resqrtcn  25911  2logb9irr  25954  leibpi  26101  log2ublem1  26105  birthday  26113  emcllem5  26158  harmonicbnd  26162  harmonicbnd2  26163  harmonicbnd3  26166  lgamgulm2  26194  lgamcvglem  26198  gamf  26201  ppiltx  26335  ppiublem1  26359  ppiub  26361  bclbnd  26437  bpos1lem  26439  bposlem8  26448  lgsquadlem2  26538  2sqlem9  26584  2sqlem10  26585  addsqnreup  26600  chebbnd1  26629  selberg2lem  26707  pntrsumo1  26722  selbergsb  26732  pntpbnd  26745  lngndxnitvndx  26813  istrkg2ld  26830  tgcgr4  26901  ttgvalOLD  27246  ttglemOLD  27248  cchhllemOLD  27264  ax5seglem7  27312  axlowdimlem4  27322  axlowdimlem6  27324  axlowdimlem7  27325  axlowdimlem10  27328  axlowdimlem13  27331  axlowdimlem16  27334  uhgr0e  27450  uhgr0  27452  upgrbi  27472  umgrbi  27480  usgr0  27619  lfuhgr1v0e  27630  usgrexmpllem  27636  usgrexmpl  27639  griedg0prc  27640  cplgr0  27801  usgrexilem  27816  cffldtocusgr  27823  rgrusgrprc  27965  rusgrprc  27966  rgrprcx  27968  rgrx0ndm  27969  usgr2pthlem  28140  pthdlem2  28145  uspgrn2crct  28182  wwlksnext  28267  wwlksnfi  28280  disjxwwlkn  28287  clwwlknondisj  28484  0ewlk  28487  0wlk  28489  0pth  28498  1pthdlem1  28508  1trld  28515  wlk2v2elem2  28529  wlk2v2e  28530  upgr3v3e3cycl  28553  upgr4cycl4dv4e  28558  dfconngr1  28561  0conngr  28565  konigsbergumgr  28624  2wspmdisj  28710  2clwwlk2clwwlk  28723  numclwwlk3lem2lem  28756  numclwwlk3lem2  28757  ex-dif  28796  ex-in  28798  ex-eprel  28806  ex-id  28807  ex-fl  28820  ex-mod  28822  ex-hash  28826  ex-fpar  28835  avril1  28836  2bornot2b  28837  0vfval  28977  vsfval  29004  ajmoi  29229  ajfuni  29230  normlem2  29482  norm3adifii  29519  hhip  29548  hlim0  29606  hlimcaui  29607  hlimf  29608  hhssnv  29635  shscli  29688  shsval2i  29758  h1de2i  29924  fh3i  29994  fh4i  29995  cm2mi  29997  qlaxr3i  30007  mayetes3i  30100  ho0f  30122  hoif  30125  hodidi  30158  ho0subi  30166  hosd1i  30193  adjmo  30203  nmopsetn0  30236  nmfnsetn0  30249  funadj  30257  funcnvadj  30264  nmcexi  30397  cnlnadjlem8  30445  nmoptri2i  30470  opsqrlem4  30514  hmopidmchi  30522  pjoci  30551  pjinvari  30562  abrexdomjm  30861  elim2ifim  30897  iundisj2f  30938  rinvf1o  30974  dfcnv2  31022  snct  31057  fzodif2  31122  iundisj2fi  31127  dp2lt10  31167  dp2ltc  31170  dplti  31188  dpgti  31189  dpexpp1  31191  gsumle  31359  xrge0slmod  31557  zarcls  31833  zartopn  31834  xrge0pluscn  31899  zlmdsOLD  31922  zlmtsetOLD  31924  qqhre  31979  esumrnmpt2  32045  esumfsup  32047  esumpcvgval  32055  hasheuni  32062  esumcvg  32063  esumcvgsum  32065  esumsup  32066  esum2d  32070  dmsigagen  32121  ldgenpisyslem3  32142  measvuni  32191  voliune  32206  volfiniune  32207  br2base  32245  dya2iocuni  32259  eulerpartlem1  32343  eulerpartlemt  32347  eulerpartgbij  32348  fib0  32375  coinfliprv  32458  ballotlem2  32464  ballotlemic  32482  ballotlem7  32511  ballotth  32513  plymul02  32534  rpsqrtcn  32582  chtvalz  32618  circlemethnat  32630  circlevma  32631  circlemethhgt  32632  hgt750lem  32640  bnj226  32722  bnj1101  32773  bnj110  32847  bnj149  32864  bnj150  32865  bnj151  32866  bnj517  32874  bnj580  32902  bnj865  32912  bnj900  32918  bnj996  32945  bnj1110  32971  bnj1133  32978  bnj1128  32979  bnj1145  32982  bnj1137  32984  bnj1171  32989  bnj1176  32994  f1resfz0f1d  33081  subfacp1lem5  33155  subfacp1lem6  33156  kur14lem9  33185  cvmcov2  33246  cvmliftlem1  33256  cvmliftlem4  33259  cvmliftlem5  33260  gonanegoal  33323  satfv0  33329  satfv0fun  33342  fmlan0  33362  gonan0  33363  fmla0disjsuc  33369  ex-sategoelel12  33398  msrfo  33517  problem5  33636  brtpid1  33674  brtpid2  33675  brtpid3  33676  logi  33709  faclimlem1  33718  axextndbi  33789  poseq  33811  sltval2  33868  noxp1o  33875  nosepnelem  33891  noetasuplem2  33946  noetainflem2  33950  0slt1s  34032  txprel  34190  relsset  34199  relbigcup  34208  fvbigcup  34213  fnsingle  34230  fvsingle  34231  snelsingles  34233  funimage  34239  fullfunfnv  34257  imagesset  34264  funtransport  34342  colinrel  34368  funray  34451  funline  34453  0hf  34488  neibastop2lem  34558  filnetlem3  34578  nrmo  34608  waj-ax  34612  lukshef-ax2  34613  arg-ax  34614  limsucncmpi  34643  dnizeq0  34664  knoppcnlem8  34689  knoppcnlem11  34692  cnndvlem1  34726  bj-babylob  34795  bj-ax12ssb  34848  bj-nnfnth  34934  bj-disjcsn  35150  bj-snsetex  35162  bj-0eltag  35177  bj-2upln0  35222  bj-2upln1upl  35223  f1omptsnlem  35516  f1omptsn  35517  icoreresf  35532  relowlssretop  35543  relowlpssretop  35544  domalom  35584  matunitlindf  35784  poimirlem3  35789  poimirlem9  35795  poimirlem16  35802  poimirlem17  35803  poimirlem18  35804  poimirlem19  35805  poimirlem20  35806  poimirlem26  35812  mblfinlem1  35823  mblfinlem2  35824  ismblfin  35827  voliunnfl  35830  cnambfre  35834  abrexdom  35897  fdc  35912  cncfres  35932  heibor1lem  35976  grposnOLD  36049  bicontr  36247  an12i  36265  tsim1  36297  ac6s6f  36340  vvdifopab  36407  brcnvrabga  36484  opabf  36505  xrnrel  36510  relcoels  36554  cnvcosseq  36567  refrelcoss3  36588  refrelcoss2  36589  symrelcoss2  36591  refrelcoss  36647  symrelcoss  36681  n0eldmqs  36768  ax13fromc9  36927  dedths  36983  renegclALT  36984  hlhilslemOLD  39960  12gcd5e1  40018  60gcd7e1  40020  lcmineqlem23  40066  dvrelog2  40079  dvrelog3  40080  dvrelog2b  40081  aks4d1p1p6  40088  aks4d1p1p7  40089  aks4d1p1  40091  sticksstones22  40131  2xp3dxp2ge1d  40169  acos1half  40177  sn-axprlem3  40193  rtprmirr  40354  moxfr  40521  mapfzcons1  40546  diophrw  40588  0dioph  40607  vdioph  40608  rabren3dioph  40644  2nn0ind  40774  rpnnen3  40861  kelac2lem  40896  frlmpwfi  40930  ifpbiidcor2  41097  iscard4  41147  sqrtcval  41256  resqrtvalex  41260  eliunov2  41294  xphe  41396  0he  41397  he0  41399  snhesn  41401  idhe  41402  frege54cor1c  41530  clsk1independent  41663  neicvgnvor  41733  amgm2d  41816  amgm3d  41817  amgm4d  41818  ismnushort  41926  lhe4.4ex1a  41954  rusbcALT  42064  ipo0  42074  ifr0  42075  vk15.4j  42155  2sb5nd  42187  dfvd1ir  42200  dfvd2anir  42211  dfvd2ir  42213  dfvd3ir  42220  dfvd3anir  42223  iden2  42241  e0bir  42404  uun2221p1  42441  uun2221p2  42442  2sb5ndVD  42537  2sb5ndALT  42559  iunconnlem2  42562  fnchoice  42579  unisn0  42609  eliincex  42667  icof  42766  supminfxr  43011  fsumiunss  43123  climlimsupcex  43317  liminfltlimsupex  43329  liminflelimsupcex  43345  xlimrel  43368  xlimfun  43403  resincncf  43423  dvnprodlem3  43496  volioc  43520  volico  43531  dmvolss  43533  volioof  43535  stoweidlem13  43561  stoweidlem34  43582  stirlinglem5  43626  stirlinglem13  43634  stirlingr  43638  fourierdlem42  43697  fourierdlem62  43716  fouriersw  43779  etransc  43831  salexct  43880  salexct2  43885  salgencntex  43889  sge0rnn0  43913  gsumge0cl  43916  sge00  43921  sge0resplit  43951  sge0reuz  43992  omeiunle  44062  0ome  44074  icoresmbl  44088  ovn0lem  44110  ovnhoilem1  44146  hspmbl  44174  ovolval5lem3  44199  nsssmfmbf  44324  mbfpsssmf  44328  smfresal  44333  smfmullem4  44339  smfpimbor1lem1  44343  smfpimbor1lem2  44344  aistia  44403  aisfina  44404  aiffnbandciffatnotciffb  44410  axorbciffatcxorb  44411  abnotbtaxb  44421  abnotataxb  44422  eusnsn  44531  aiotaval  44598  aiota0ndef  44600  fundcmpsurinjimaid  44874  ichv  44912  ichf  44913  ichid  44914  icht  44915  ichcircshi  44917  icheq  44925  spr0nelg  44939  m3prm  45055  m7prm  45063  0noddALTV  45152  2noddALTV  45156  341fppr2  45197  9fppr8  45200  nfermltl8rev  45205  nfermltl2rev  45206  nfermltlrev  45207  sbgoldbo  45250  nnsum3primes4  45251  evengpop3  45261  oddinmgm  45380  nn0mnd  45384  2zrngamgm  45508  2zrngaabl  45513  2zrngmmgm  45515  2zrngnring  45521  fldhmsubc  45653  fldhmsubcALTV  45671  eliunxp2  45680  zlmodzxzldeplem  45850  zlmodzxzldep  45856  ldepslinc  45861  rrx2xpreen  46076  rrx2plordisom  46080  line2ylem  46108  line2  46109  line2x  46111  inlinecirc02plem  46143  mosn  46169  mof0  46176  mof0ALT  46178  f1omo  46199  prstclevalOLD  46361  prstcocvalOLD  46364  ex-gte  46442  empty-surprise  46497  eximp-surprise2  46500  amgmw2d  46519