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  401  mpbir2an  709  imorri  853  orri  860  mpbir3an  1341  xorexmid  1527  tru  1545  had1  1604  nic-mpALT  1674  nic-ax  1675  nic-axALT  1676  nfi  1790  mpgbir  1801  nfxfr  1855  19.35ri  1882  ax5e  1915  ax6ev  1973  sbt  2069  equsb1v  2103  ax13  2373  ax13ALT  2423  moanmo  2617  axi12  2700  axbnd  2701  axexte  2703  axextmo  2706  nulmo  2707  vexw  2714  eqeltri  2828  nfcxfr  2900  neir  2942  neirr  2948  eqnetri  3010  nelir  3048  mprgbir  3067  cbvrexdva2OLD  3323  issetri  3462  moeq  3668  rmoeq  3699  cdeqi  3726  eqsstri  3981  3sstr4i  3990  rmo0  4324  rabnc  4352  reuprg  4669  tpid1  4734  tpid2  4736  mosneq  4805  pwv  4867  uni0  4901  int0  4928  eqbrtri  5131  tr0  5240  trv  5241  zfrep4  5258  axnulALT  5266  0ex  5269  inex1  5279  elpwi2  5308  elpwi2OLD  5309  0elpw  5316  axpow2  5327  axpow3  5328  dvdemo1  5333  vpwex  5337  zfpair2  5390  exss  5425  brv  5434  opwo0id  5459  moop2  5464  0sn0ep  5546  po0  5567  epse  5621  relxp  5656  rel0  5760  relopabiv  5781  relopabi  5783  relopabiALT  5784  eliunxp  5798  opeliunxp2  5799  dmi  5882  dmep  5884  xpidtr  6081  xpima  6139  dmsn0  6166  cnvsn0  6167  0elon  6376  funmpt  6544  funmpt2  6545  funcnv0  6572  isarep2  6597  fresaunres2  6719  f0  6728  f10d  6823  f1o00  6824  f1oi  6827  f1osn  6829  brprcneu  6837  brprcneuALT  6838  opabiotafun  6927  fvopab3ig  6949  opabex  7175  eufnfv  7184  isof1oopb  7275  ncanth  7316  mpofun  7485  mpofunOLD  7486  reldmmpo  7495  ovid  7501  ovidig  7502  ovidi  7503  ovig  7506  ov3  7522  caovmo  7596  relmptopab  7608  porpss  7669  uniex2  7680  tfinds2  7805  finds  7840  finds2  7842  oprabex  7914  oprabex3  7915  f1stres  7950  f2ndres  7951  relmpoopab  8031  fsplitfpar  8055  poseq  8095  opeliunxp2f  8146  tpos0  8192  wfrrelOLD  8265  wfrlem14OLD  8273  wfrlem16OLD  8275  issmo  8299  tfrlem6  8333  tfrlem8  8335  tfrlem16  8344  tfr1a  8345  tfr1  8348  tz7.44lem1  8356  seqomlem2  8402  seqomlem3  8403  seqomlem4  8404  fnseqom  8406  ord3  8434  0lt1o  8455  0we1  8457  naddf  8632  eqer  8690  ecopover  8767  mapsnf1o3  8840  ssdomg  8947  en0  8964  en0OLD  8965  en0r  8967  ensn1  8968  ensn1OLD  8969  snfi  8995  enrefnn  8998  xpcomf1o  9012  map2xp  9098  limensuci  9104  1sdom2  9191  sdom1  9193  sdom1OLD  9194  unblem4  9249  fidomdm  9280  marypha1lem  9378  hartogslem1  9487  hartogs  9489  card2on  9499  nelaneq  9544  epinid0  9545  ruALT  9548  disjcsn  9549  elnanel  9552  cnvepnep  9553  inf2  9568  inf3lem6  9578  infeq5i  9581  zfinf2  9587  cantnflt  9617  cnfcom  9645  trcl  9673  tz9.1c  9675  tc2  9687  r1funlim  9711  r1fnon  9712  karden  9840  tskwe  9895  cardprclem  9924  pm54.43  9946  r0weon  9957  iunmapdisj  9968  alephfnon  10010  alephfplem4  10052  alephfp  10053  alephval3  10055  kmlem2  10096  dju1dif  10117  ackbij1  10183  ackbij2lem2  10185  ackbij2  10188  infpssrlem3  10250  hsmexlem4  10374  hsmexlem5  10375  ac2  10406  axac3  10409  ac6  10425  axdclem2  10465  dmct  10469  ondomon  10508  alephsucpw  10515  pwcfsdom  10528  cfpwsdom  10529  smobeth  10531  axpowndlem3  10544  zfcndun  10560  zfcndpow  10561  zfcndinf  10563  zfcndac  10564  wunex2  10683  uniwun  10685  wuncval2  10692  grur1  10765  axgroth5  10769  axgroth2  10770  axgroth6  10773  axgroth3  10776  grothtsk  10780  inaprc  10781  ltsopi  10833  dmaddpi  10835  dmmulpi  10836  1lt2pi  10850  nqerf  10875  addnqf  10893  mulnqf  10894  1lt2nq  10918  m1p1sr  11037  m1m1sr  11038  0lt1sr  11040  axaddf  11090  axmulf  11091  ax1cn  11094  subaddrii  11499  ixi  11793  recgt0ii  12070  nn1suc  12184  neg1lt0  12279  4d2e2  12332  arch  12419  un0mulcl  12456  pnf0xnn0  12501  3halfnz  12591  nummac  12672  indstr  12850  mnfltpnf  13056  ioof  13374  0nelfz1  13470  fzp1disj  13510  fzp1nel  13535  fzof  13579  om2uzrani  13867  om2uzf1oi  13868  uzrdglem  13872  uzrdgfni  13873  uzrdg0i  13874  ltwenn  13877  hashgf1o  13886  axdc4uzlem  13898  sq0  14106  irec  14115  facmapnn  14195  hashkf  14242  hashfxnn0  14247  hashf  14248  hash0  14277  prhash2ex  14309  hashsslei  14336  hashxplem  14343  hashbclem  14361  hashf1lem1  14365  hashf1lem1OLD  14366  s1dm  14508  eqs1  14512  ccat2s1p1  14529  cats1un  14621  revs1  14665  0csh0  14693  cshw1  14722  cats1fvn  14759  funcnvs1  14813  pfx2  14848  relexp0g  14919  relexpsucnnr  14922  rtrclreclem1  14954  dfrtrclrec2  14955  rtrclreclem2  14956  rtrclreclem4  14958  dfrtrcl2  14959  climmo  15451  fsumcom2  15670  ackbijnn  15724  incexclem  15732  infcvgaux1i  15753  fprodcom2  15878  bpolylem  15942  bpoly3  15952  bpoly4  15953  efcvgfsum  15979  cos1bnd  16080  cos2bnd  16081  znnen  16105  qnnen  16106  aleph1re  16138  3dvds  16224  n2dvdsm1  16262  divalglem5  16290  flodddiv4  16306  sadcaddlem  16348  sadadd2lem  16350  sadadd3  16352  sadaddlem  16357  lcmf0  16521  lcmfunsnlem2lem1  16525  lcmfunsnlem2  16527  coprmprod  16548  coprmproddvdslem  16549  2prm  16579  3lcm2e6  16618  phicl2  16651  pockthi  16790  unbenlem  16791  prmrec  16805  vdwlem13  16876  vdwnn  16881  ramcl2  16899  prmgapprmo  16945  mod2xnegi  16954  modsubi  16955  structcnvcnv  17036  strleun  17040  setsres  17061  strfv  17087  starvndxnbasendx  17199  starvndxnplusgndx  17200  starvndxnmulrndx  17201  scandxnbasendx  17211  scandxnplusgndx  17212  scandxnmulrndx  17213  vscandxnbasendx  17216  vscandxnplusgndx  17217  vscandxnmulrndx  17218  vscandxnscandx  17219  ipndxnbasendx  17227  ipndxnplusgndx  17228  ipndxnmulrndx  17229  slotsdifipndx  17230  tsetndxnplusgndx  17252  tsetndxnmulrndx  17253  tsetndxnstarvndx  17254  slotstnscsi  17255  plendxnplusgndx  17266  plendxnmulrndx  17267  plendxnscandx  17268  plendxnvscandx  17269  slotsdifplendx  17270  basendxnocndx  17278  plendxnocndx  17279  dsndxnplusgndx  17285  dsndxnmulrndx  17286  slotsdnscsi  17287  dsndxntsetndx  17288  slotsdifdsndx  17289  unifndxntsetndx  17295  slotsdifunifndx  17296  slotsdifplendx2  17312  slotsdifocndx  17313  0rest  17325  firest  17328  restid  17329  prdsval  17351  prdsbas  17353  prdsplusg  17354  prdsmulr  17355  prdsvsca  17356  imasaddfnlem  17424  imasvscafn  17433  oppchomfvalOLD  17609  oppcbasOLD  17614  2oppchomf  17620  rescbasOLD  17727  resccoOLD  17731  rescabsOLD  17733  0ssc  17737  0subcat  17738  idfucl  17781  homarel  17936  dmaf  17949  cdaf  17950  setc2ohom  17995  catcfuccl  18019  catcfucclOLD  18020  relxpchom  18083  catcxpccl  18109  catcxpcclOLD  18110  oppchofcl  18163  oyoncl  18173  odubasOLD  18195  letsr  18496  mgmidmo  18529  efmndmgm  18709  smndex1ibas  18724  smndex1mgm  18731  smndex1mnd  18734  smndex2dbas  18738  smndex2dnrinv  18739  smndex2hbas  18740  pwmnd  18761  releqg  18991  ga0  19092  oppglemOLD  19143  psgnunilem3  19292  psgnunilem4  19293  pmtrsn  19315  efgval  19513  efger  19514  efgsval2  19529  efgsp1  19533  efgsfo  19535  efgredleme  19539  efgredlem  19543  efgred  19544  cygctb  19683  gsum2d2lem  19764  gsum2d2  19765  gsumcom2  19766  dprd2d2  19837  pgpfaclem1  19874  mgplemOLD  19915  mgpressOLD  19926  opprlemOLD  20069  reldvdsr  20087  00lsp  20499  sralemOLD  20698  srascaOLD  20706  sravscaOLD  20708  cnfldfun  20845  cnfldfunALT  20846  cnfldfunALTOLD  20847  xrsmgm  20869  znbaslemOLD  20979  resubdrg  21049  ocv0  21118  cssval  21123  thlbasOLD  21138  thlleOLD  21140  islinds2  21256  psrvscafval  21395  opsrbaslemOLD  21488  psrbag0  21507  00ply1bas  21648  ply1plusgfvi  21650  matscaOLD  21800  m2detleib  22017  tgdom  22365  tgidm  22367  indistps2ALT  22402  restbas  22546  resttopon  22549  rest0  22557  leordtval2  22600  iocpnfordt  22603  icomnfordt  22604  iooordt  22605  ist1-3  22737  1stcfb  22833  comppfsc  22920  1stckgen  22942  ptbasfi  22969  dfac14  23006  opnfbas  23230  hauspwpwf1  23375  alexsubALT  23439  ptcmplem5  23444  cnextrel  23451  ust0  23608  tuslemOLD  23656  0met  23756  prdsdsf  23757  prdsxmetlem  23758  prdsmet  23760  setsmsbasOLD  23866  setsmsdsOLD  23868  prdsbl  23884  tngdsOLD  24049  qtopbaslem  24159  xrtgioo  24206  xrsdsre  24210  zcld  24213  recld2  24214  reperflem  24218  retopconn  24229  iccpnfcnv  24344  bndth  24358  nmoleub2lem2  24516  zclmncvs  24549  recmet  24724  resscdrg  24759  ishl2  24771  recms  24781  volf  24930  iundisj2  24950  volsup  24957  icombl  24965  ioombl  24966  ismbf3d  25055  0plef  25073  0pledm  25074  itg1ge0  25087  mbfi1fseqlem5  25121  itg2addlem  25160  reldv  25271  limciun  25295  dvexp  25354  dveflem  25380  lhop1lem  25414  lhop  25417  elply2  25594  elplyd  25600  ply1term  25602  ply0  25606  plymullem  25614  qaa  25720  pserulm  25818  pserdvlem2  25824  efcn  25839  sincosq1lem  25891  tangtx  25899  sincos4thpi  25907  pigt3  25911  pige3ALT  25913  efif1olem4  25938  logf1o  25957  relogf1o  25959  log1  25978  loge  25979  relogiso  25990  dvrelog  26029  relogcn  26030  logcn  26039  cxpcn3  26138  resqrtcn  26139  2logb9irr  26182  leibpi  26329  log2ublem1  26333  birthday  26341  emcllem5  26386  harmonicbnd  26390  harmonicbnd2  26391  harmonicbnd3  26394  lgamgulm2  26422  lgamcvglem  26426  gamf  26429  ppiltx  26563  ppiublem1  26587  ppiub  26589  bclbnd  26665  bpos1lem  26667  bposlem8  26676  lgsquadlem2  26766  2sqlem9  26812  2sqlem10  26813  addsqnreup  26828  chebbnd1  26857  selberg2lem  26935  pntrsumo1  26950  selbergsb  26960  pntpbnd  26973  sltval2  27041  noxp1o  27048  nosepnelem  27064  noetasuplem2  27119  noetainflem2  27123  0slt1s  27211  addsf  27335  lngndxnitvndx  27448  istrkg2ld  27465  tgcgr4  27536  ttgvalOLD  27881  ttglemOLD  27883  cchhllemOLD  27899  ax5seglem7  27947  axlowdimlem4  27957  axlowdimlem6  27959  axlowdimlem7  27960  axlowdimlem10  27963  axlowdimlem13  27966  axlowdimlem16  27969  uhgr0e  28085  uhgr0  28087  upgrbi  28107  umgrbi  28115  usgr0  28254  lfuhgr1v0e  28265  usgrexmpllem  28271  usgrexmpl  28274  griedg0prc  28275  cplgr0  28436  usgrexilem  28451  cffldtocusgr  28458  rgrusgrprc  28600  rusgrprc  28601  rgrprcx  28603  rgrx0ndm  28604  usgr2pthlem  28774  pthdlem2  28779  uspgrn2crct  28816  wwlksnext  28901  clwwlknondisj  29118  0ewlk  29121  0wlk  29123  0pth  29132  1pthdlem1  29142  1trld  29149  wlk2v2elem2  29163  wlk2v2e  29164  upgr3v3e3cycl  29187  upgr4cycl4dv4e  29192  dfconngr1  29195  0conngr  29199  konigsbergumgr  29258  2wspmdisj  29344  2clwwlk2clwwlk  29357  numclwwlk3lem2lem  29390  numclwwlk3lem2  29391  ex-dif  29430  ex-in  29432  ex-eprel  29440  ex-id  29441  ex-fl  29454  ex-mod  29456  ex-hash  29460  ex-fpar  29469  avril1  29470  2bornot2b  29471  0vfval  29611  vsfval  29638  ajmoi  29863  ajfuni  29864  normlem2  30116  norm3adifii  30153  hhip  30182  hlim0  30240  hlimcaui  30241  hlimf  30242  hhssnv  30269  shscli  30322  shsval2i  30392  h1de2i  30558  fh3i  30628  fh4i  30629  cm2mi  30631  qlaxr3i  30641  mayetes3i  30734  ho0f  30756  hoif  30759  hodidi  30792  ho0subi  30800  hosd1i  30827  adjmo  30837  nmopsetn0  30870  nmfnsetn0  30883  funadj  30891  funcnvadj  30898  nmcexi  31031  cnlnadjlem8  31079  nmoptri2i  31104  opsqrlem4  31148  hmopidmchi  31156  pjoci  31185  pjinvari  31196  abrexdomjm  31497  elim2ifim  31531  iundisj2f  31575  rinvf1o  31611  dfcnv2  31659  snct  31698  fzodif2  31763  iundisj2fi  31768  dp2lt10  31810  dp2ltc  31813  dplti  31831  dpgti  31832  dpexpp1  31834  gsumle  32002  xrge0slmod  32211  zarcls  32544  zartopn  32545  xrge0pluscn  32610  zlmdsOLD  32633  zlmtsetOLD  32635  qqhre  32690  esumrnmpt2  32756  esumfsup  32758  esumpcvgval  32766  hasheuni  32773  esumcvg  32774  esumcvgsum  32776  esumsup  32777  esum2d  32781  dmsigagen  32832  ldgenpisyslem3  32853  measvuni  32902  voliune  32917  volfiniune  32918  br2base  32958  dya2iocuni  32972  eulerpartlem1  33056  eulerpartlemt  33060  eulerpartgbij  33061  fib0  33088  coinfliprv  33171  ballotlem2  33177  ballotlemic  33195  ballotlem7  33224  ballotth  33226  plymul02  33247  rpsqrtcn  33295  chtvalz  33331  circlemethnat  33343  circlevma  33344  circlemethhgt  33345  hgt750lem  33353  bnj226  33435  bnj1101  33485  bnj110  33559  bnj149  33576  bnj150  33577  bnj151  33578  bnj517  33586  bnj580  33614  bnj865  33624  bnj900  33630  bnj996  33657  bnj1110  33683  bnj1133  33690  bnj1128  33691  bnj1145  33694  bnj1137  33696  bnj1171  33701  bnj1176  33706  f1resfz0f1d  33793  subfacp1lem5  33865  subfacp1lem6  33866  kur14lem9  33895  cvmcov2  33956  cvmliftlem1  33966  cvmliftlem4  33969  cvmliftlem5  33970  gonanegoal  34033  satfv0  34039  satfv0fun  34052  fmlan0  34072  gonan0  34073  fmla0disjsuc  34079  ex-sategoelel12  34108  msrfo  34227  problem5  34344  brtpid1  34379  brtpid2  34380  brtpid3  34381  logi  34393  faclimlem1  34402  axextndbi  34465  txprel  34540  relsset  34549  relbigcup  34558  fvbigcup  34563  fnsingle  34580  fvsingle  34581  snelsingles  34583  funimage  34589  fullfunfnv  34607  imagesset  34614  funtransport  34692  colinrel  34718  funray  34801  funline  34803  0hf  34838  neibastop2lem  34908  filnetlem3  34928  nrmo  34958  waj-ax  34962  lukshef-ax2  34963  arg-ax  34964  limsucncmpi  34993  dnizeq0  35014  knoppcnlem8  35039  knoppcnlem11  35042  cnndvlem1  35076  bj-babylob  35145  bj-ax12ssb  35198  bj-nnfnth  35284  bj-snsetex  35507  bj-0eltag  35522  bj-2upln0  35567  bj-2upln1upl  35568  bj-snexg  35578  bj-unexg  35582  bj-adjg1  35587  f1omptsnlem  35880  f1omptsn  35881  icoreresf  35896  relowlssretop  35907  relowlpssretop  35908  domalom  35948  matunitlindf  36149  poimirlem3  36154  poimirlem9  36160  poimirlem16  36167  poimirlem17  36168  poimirlem18  36169  poimirlem19  36170  poimirlem20  36171  poimirlem26  36177  mblfinlem1  36188  mblfinlem2  36189  ismblfin  36192  voliunnfl  36195  cnambfre  36199  abrexdom  36262  fdc  36277  cncfres  36297  heibor1lem  36341  grposnOLD  36414  bicontr  36612  an12i  36630  tsim1  36662  ac6s6f  36705  vvdifopab  36793  brcnvrabga  36876  opabf  36902  xrnrel  36908  relcoels  36959  cnvcosseq  36972  refrelcoss3  36998  refrelcoss2  36999  symrelcoss2  37001  refrelcoss  37058  symrelcoss  37095  n0eldmqs  37183  ax13fromc9  37441  dedths  37497  renegclALT  37498  hlhilslemOLD  40475  12gcd5e1  40533  60gcd7e1  40535  lcmineqlem23  40581  dvrelog2  40594  dvrelog3  40595  dvrelog2b  40596  aks4d1p1p6  40603  aks4d1p1p7  40604  aks4d1p1  40606  sticksstones22  40649  2xp3dxp2ge1d  40687  acos1half  40695  sn-axprlem3  40710  rtprmirr  40891  moxfr  41073  mapfzcons1  41098  diophrw  41140  0dioph  41159  vdioph  41160  rabren3dioph  41196  2nn0ind  41327  rpnnen3  41414  kelac2lem  41449  frlmpwfi  41483  oaordnrex  41688  omnord1ex  41697  oenord1ex  41708  oaomoencom  41710  ifpbiidcor2  41877  iscard4  41927  sqrtcval  42035  resqrtvalex  42039  eliunov2  42073  xphe  42175  0he  42176  he0  42178  snhesn  42180  idhe  42181  frege54cor1c  42309  clsk1independent  42440  neicvgnvor  42510  amgm2d  42593  amgm3d  42594  amgm4d  42595  ismnushort  42703  lhe4.4ex1a  42731  rusbcALT  42841  ipo0  42851  ifr0  42852  vk15.4j  42932  2sb5nd  42964  dfvd1ir  42977  dfvd2anir  42988  dfvd2ir  42990  dfvd3ir  42997  dfvd3anir  43000  iden2  43018  e0bir  43181  uun2221p1  43218  uun2221p2  43219  2sb5ndVD  43314  2sb5ndALT  43336  iunconnlem2  43339  fnchoice  43356  unisn0  43384  eliincex  43442  icof  43561  fnmptif  43615  supminfxr  43819  rexanuz2nf  43848  fsumiunss  43936  climlimsupcex  44130  liminfltlimsupex  44142  liminflelimsupcex  44158  xlimrel  44181  xlimfun  44216  resincncf  44236  dvnprodlem3  44309  volioc  44333  volico  44344  dmvolss  44346  volioof  44348  stoweidlem13  44374  stoweidlem34  44395  stirlinglem5  44439  stirlinglem13  44447  stirlingr  44451  fourierdlem42  44510  fourierdlem62  44529  fouriersw  44592  etransc  44644  salexct  44695  salexct2  44700  salgencntex  44704  sge0rnn0  44729  gsumge0cl  44732  sge00  44737  sge0resplit  44767  sge0reuz  44808  omeiunle  44878  0ome  44890  icoresmbl  44904  ovn0lem  44926  ovnhoilem1  44962  hspmbl  44990  nsssmfmbf  45140  mbfpsssmf  45144  smfresal  45149  smfmullem4  45155  smfpimbor1lem1  45159  smfpimbor1lem2  45160  aistia  45252  aisfina  45253  aiffnbandciffatnotciffb  45259  axorbciffatcxorb  45260  abnotbtaxb  45270  abnotataxb  45271  eusnsn  45380  aiotaval  45447  aiota0ndef  45449  fundcmpsurinjimaid  45723  ichv  45761  ichf  45762  ichid  45763  icht  45764  ichcircshi  45766  icheq  45774  spr0nelg  45788  m3prm  45904  m7prm  45912  0noddALTV  46001  2noddALTV  46005  341fppr2  46046  9fppr8  46049  nfermltl8rev  46054  nfermltl2rev  46055  nfermltlrev  46056  sbgoldbo  46099  nnsum3primes4  46100  evengpop3  46110  oddinmgm  46229  nn0mnd  46233  2zrngamgm  46357  2zrngaabl  46362  2zrngmmgm  46364  2zrngnring  46370  fldhmsubc  46502  fldhmsubcALTV  46520  eliunxp2  46529  zlmodzxzldeplem  46699  zlmodzxzldep  46705  ldepslinc  46710  rrx2xpreen  46925  rrx2plordisom  46929  line2ylem  46957  line2  46958  line2x  46960  inlinecirc02plem  46992  mosn  47017  mof0  47024  mof0ALT  47026  f1omo  47047  prstclevalOLD  47209  prstcocvalOLD  47212  ex-gte  47294  empty-surprise  47349  eximp-surprise2  47352  amgmw2d  47371