Theorem mpbir 233

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 230	. 2 ⊢ (𝜓 → 𝜑)
4	1, 3	ax-mp 5	1 ⊢ 𝜑

Syntax hints:   ↔ wb 208

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 209

This theorem is referenced by:  pm5.74ri  274  con4bii  323  imnani  403  mpbir2an  709  imorri  851  orri  858  mpbir3an  1337  xorexmid  1519  tru  1541  had1  1604  nic-mpALT  1673  nic-ax  1674  nic-axALT  1675  nfi  1789  mpgbir  1800  nfxfr  1853  19.35ri  1880  ax5e  1913  ax6ev  1972  sbt  2071  equsb1v  2112  ax13  2393  ax13ALT  2447  moanmo  2707  axi12  2791  axbnd  2792  axexte  2794  axextmo  2797  nulmo  2798  vexw  2805  eqeltri  2909  nfcxfr  2975  neir  3019  neirr  3025  eqnetri  3086  nelir  3126  mprgbir  3153  cbvrexdva2  3457  vexOLD  3498  issetri  3510  moeq  3698  rmoeq  3729  cdeqi  3756  eqsstri  4001  3sstr4i  4010  rmo0  4319  rabnc  4341  reuprg  4639  tpid1  4704  tpid2  4706  mosneq  4773  pwv  4835  uni0  4866  int0  4890  eqbrtri  5087  tr0  5183  trv  5184  zfrep4  5200  axnulALT  5208  0ex  5211  inex1  5221  elpwi2  5249  0elpw  5256  axpow2  5268  axpow3  5269  dvdemo1  5274  vpwex  5278  zfpair2  5331  exss  5355  brv  5364  opwo0id  5387  moop2  5392  pwundifOLD  5457  0sn0ep  5470  po0  5490  epse  5538  relxp  5573  rel0  5672  relopabiv  5693  relopabi  5694  relopabiALT  5695  eliunxp  5708  opeliunxp2  5709  dmi  5791  dmep  5793  domepOLD  5794  xpidtr  5982  xpima  6039  dmsn0  6066  cnvsn0  6067  0elon  6244  funmpt  6393  funmpt2  6394  funcnv0  6420  isarep2  6443  fresaunres2  6550  f0  6560  f10d  6648  f1o00  6649  f1oi  6652  f1osn  6654  brprcneu  6662  opabiotafun  6744  fvopab3ig  6764  opabex  6983  mptexgf  6985  eufnfv  6991  isof1oopb  7078  ncanth  7112  mpofun  7276  reldmmpo  7285  ovid  7291  ovidig  7292  ovidi  7293  ovig  7296  ov3  7311  caovmo  7385  relmptopab  7395  porpss  7453  uniex2  7464  tfinds2  7578  finds  7608  finds2  7610  oprabex  7677  oprabex3  7678  f1stres  7713  f2ndres  7714  relmpoopab  7789  fsplitfpar  7814  opeliunxp2f  7876  tpos0  7922  wfrrel  7960  wfrlem14  7968  wfrlem16  7970  issmo  7985  tfrlem6  8018  tfrlem8  8020  tfrlem16  8029  tfr1a  8030  tfr1  8033  tz7.44lem1  8041  seqomlem2  8087  seqomlem3  8088  seqomlem4  8089  fnseqom  8091  0lt1o  8129  0we1  8131  eqer  8324  ecopover  8401  mapsnf1o3  8459  ssdomg  8555  ensn1  8573  snfi  8594  xpcomf1o  8606  map2xp  8687  limensuci  8693  sdom1  8718  unblem4  8773  fidomdm  8801  marypha1lem  8897  hartogslem1  9006  hartogs  9008  card2on  9018  nelaneq  9063  epinid0  9064  ruALT  9067  elnanel  9070  cnvepnep  9071  inf2  9086  inf3lem6  9096  infeq5i  9099  zfinf2  9105  cantnflt  9135  cnfcom  9163  trcl  9170  tz9.1c  9172  tc2  9184  r1funlim  9195  r1fnon  9196  karden  9324  tskwe  9379  cardprclem  9408  pm54.43  9429  r0weon  9438  iunmapdisj  9449  alephfnon  9491  alephfplem4  9533  alephfp  9534  alephval3  9536  kmlem2  9577  dju1dif  9598  ackbij1  9660  ackbij2lem2  9662  ackbij2  9665  infpssrlem3  9727  hsmexlem4  9851  hsmexlem5  9852  ac2  9883  axac3  9886  ac6  9902  axdclem2  9942  dmct  9946  ondomon  9985  alephsucpw  9992  pwcfsdom  10005  cfpwsdom  10006  smobeth  10008  axpowndlem3  10021  zfcndun  10037  zfcndpow  10038  zfcndinf  10040  zfcndac  10041  wunex2  10160  uniwun  10162  wuncval2  10169  grur1  10242  axgroth5  10246  axgroth2  10247  axgroth6  10250  axgroth3  10253  grothtsk  10257  inaprc  10258  ltsopi  10310  dmaddpi  10312  dmmulpi  10313  1lt2pi  10327  nqerf  10352  addnqf  10370  mulnqf  10371  1lt2nq  10395  m1p1sr  10514  m1m1sr  10515  0lt1sr  10517  axaddf  10567  axmulf  10568  ax1cn  10571  subaddrii  10975  ixi  11269  recgt0ii  11546  nn1suc  11660  neg1lt0  11755  4d2e2  11808  arch  11895  un0mulcl  11932  pnf0xnn0  11975  3halfnz  12062  nummac  12144  indstr  12317  mnfltpnf  12522  ioof  12836  0nelfz1  12927  fzp1disj  12967  fzp1nel  12992  fzof  13036  om2uzrani  13321  om2uzf1oi  13322  uzrdglem  13326  uzrdgfni  13327  uzrdg0i  13328  ltwenn  13331  hashgf1o  13340  axdc4uzlem  13352  sq0  13556  irec  13565  facmapnn  13646  hashkf  13693  hashfxnn0  13698  hashf  13699  hash0  13729  prhash2ex  13761  hashsslei  13788  hashxplem  13795  hashbclem  13811  hashf1lem1  13814  wrdexgOLD  13873  s1dm  13962  eqs1  13966  ccat2s1p1  13985  cats1un  14083  revs1  14127  0csh0  14155  cshw1  14184  cats1fvn  14220  funcnvs1  14274  pfx2  14309  relexp0g  14381  relexpsucnnr  14384  dfrtrclrec2  14416  rtrclreclem1  14417  rtrclreclem2  14418  rtrclreclem4  14420  dfrtrcl2  14421  climmo  14914  fsumcom2  15129  ackbijnn  15183  incexclem  15191  infcvgaux1i  15212  fprodcom2  15338  bpolylem  15402  bpoly3  15412  bpoly4  15413  efcvgfsum  15439  cos1bnd  15540  cos2bnd  15541  znnen  15565  qnnen  15566  aleph1re  15598  3dvds  15680  n2dvdsm1  15719  n2dvds3OLD  15722  divalglem5  15748  flodddiv4  15764  sadcaddlem  15806  sadadd2lem  15808  sadadd3  15810  sadaddlem  15815  lcmf0  15978  lcmfunsnlem2lem1  15982  lcmfunsnlem2  15984  coprmprod  16005  coprmproddvdslem  16006  2prm  16036  3lcm2e6  16072  phicl2  16105  pockthi  16243  unbenlem  16244  prmrec  16258  vdwlem13  16329  vdwnn  16334  ramcl2  16352  prmgapprmo  16398  mod2xnegi  16407  modsubi  16408  structcnvcnv  16497  setsres  16525  strfv  16531  strleun  16591  0rest  16703  firest  16706  restid  16707  prdsval  16728  prdsbas  16730  prdsplusg  16731  prdsmulr  16732  prdsvsca  16733  imasaddfnlem  16801  imasvscafn  16810  oppchomfval  16984  oppcbas  16988  2oppchomf  16994  rescbas  17099  rescco  17102  rescabs  17103  0ssc  17107  0subcat  17108  idfucl  17151  homarel  17296  dmaf  17309  cdaf  17310  catcfuccl  17369  relxpchom  17431  catcxpccl  17457  oppchofcl  17510  oyoncl  17520  odubas  17743  letsr  17837  mgmidmo  17870  efmndmgm  18050  smndex1ibas  18065  smndex1mgm  18072  smndex1mnd  18075  smndex2dbas  18079  smndex2dnrinv  18080  smndex2hbas  18081  pwmnd  18102  releqg  18327  ga0  18428  oppglem  18478  psgnunilem3  18624  psgnunilem4  18625  pmtrsn  18647  efgval  18843  efger  18844  efgsval2  18859  efgsp1  18863  efgsfo  18865  efgredleme  18869  efgredlem  18873  efgred  18874  cygctb  19012  gsum2d2lem  19093  gsum2d2  19094  gsumcom2  19095  dprd2d2  19166  pgpfaclem1  19203  mgplem  19244  mgpress  19250  opprlem  19378  reldvdsr  19394  00lsp  19753  sralem  19949  srasca  19953  sravsca  19954  psrvscafval  20170  opsrbaslem  20258  psrbag0  20274  00ply1bas  20408  ply1plusgfvi  20410  cnfldfun  20557  cnfldfunALT  20558  xrsmgm  20580  zlmsca  20668  znbaslem  20685  resubdrg  20752  ocv0  20821  cssval  20826  thlbas  20840  thlle  20841  islinds2  20957  matsca  21024  m2detleib  21240  tgdom  21586  tgidm  21588  indistps2ALT  21622  restbas  21766  resttopon  21769  rest0  21777  leordtval2  21820  iocpnfordt  21823  icomnfordt  21824  iooordt  21825  ist1-3  21957  1stcfb  22053  comppfsc  22140  1stckgen  22162  ptbasfi  22189  dfac14  22226  opnfbas  22450  hauspwpwf1  22595  alexsubALT  22659  ptcmplem5  22664  cnextrel  22671  ust0  22828  tuslem  22876  0met  22976  prdsdsf  22977  prdsxmetlem  22978  prdsmet  22980  setsmsbas  23085  setsmsds  23086  prdsbl  23101  tngds  23257  qtopbaslem  23367  xrtgioo  23414  xrsdsre  23418  zcld  23421  recld2  23422  reperflem  23426  retopconn  23437  iccpnfcnv  23548  bndth  23562  nmoleub2lem2  23720  zclmncvs  23752  recmet  23926  resscdrg  23961  ishl2  23973  recms  23983  volf  24130  iundisj2  24150  volsup  24157  icombl  24165  ioombl  24166  ismbf3d  24255  0plef  24273  0pledm  24274  itg1ge0  24287  mbfi1fseqlem5  24320  itg2addlem  24359  reldv  24468  limciun  24492  dvexp  24550  dveflem  24576  lhop1lem  24610  lhop  24613  elply2  24786  elplyd  24792  ply1term  24794  ply0  24798  plymullem  24806  qaa  24912  pserulm  25010  pserdvlem2  25016  efcn  25031  sincosq1lem  25083  tangtx  25091  sincos4thpi  25099  pigt3  25103  pige3ALT  25105  efif1olem4  25129  logf1o  25148  relogf1o  25150  log1  25169  loge  25170  relogiso  25181  dvrelog  25220  relogcn  25221  logcn  25230  cxpcn3  25329  resqrtcn  25330  2logb9irr  25373  leibpi  25520  log2ublem1  25524  birthday  25532  emcllem5  25577  harmonicbnd  25581  harmonicbnd2  25582  harmonicbnd3  25585  lgamgulm2  25613  lgamcvglem  25617  gamf  25620  ppiltx  25754  ppiublem1  25778  ppiub  25780  bclbnd  25856  bpos1lem  25858  bposlem8  25867  lgsquadlem2  25957  2sqlem9  26003  2sqlem10  26004  addsqnreup  26019  chebbnd1  26048  selberg2lem  26126  pntrsumo1  26141  selbergsb  26151  pntpbnd  26164  istrkg2ld  26246  tgcgr4  26317  ttgval  26661  ttglem  26662  cchhllem  26673  ax5seglem7  26721  axlowdimlem4  26731  axlowdimlem6  26733  axlowdimlem7  26734  axlowdimlem10  26737  axlowdimlem13  26740  axlowdimlem16  26743  uhgr0e  26856  uhgr0  26858  upgrbi  26878  umgrbi  26886  usgr0  27025  lfuhgr1v0e  27036  usgrexmpllem  27042  usgrexmpl  27045  griedg0prc  27046  cplgr0  27207  usgrexilem  27222  cffldtocusgr  27229  rgrusgrprc  27371  rusgrprc  27372  rgrprcx  27374  rgrx0ndm  27375  usgr2pthlem  27544  pthdlem2  27549  uspgrn2crct  27586  wwlksnext  27671  wwlksnfi  27684  wwlksnfiOLD  27685  disjxwwlkn  27692  clwwlknondisj  27890  0ewlk  27893  0wlk  27895  0pth  27904  1pthdlem1  27914  1trld  27921  wlk2v2elem2  27935  wlk2v2e  27936  upgr3v3e3cycl  27959  upgr4cycl4dv4e  27964  dfconngr1  27967  0conngr  27971  konigsbergumgr  28030  2wspmdisj  28116  2clwwlk2clwwlk  28129  numclwwlk3lem2lem  28162  numclwwlk3lem2  28163  ex-dif  28202  ex-in  28204  ex-eprel  28212  ex-id  28213  ex-fl  28226  ex-mod  28228  ex-hash  28232  ex-fpar  28241  avril1  28242  2bornot2b  28243  0vfval  28383  vsfval  28410  ajmoi  28635  ajfuni  28636  normlem2  28888  norm3adifii  28925  hhip  28954  hlim0  29012  hlimcaui  29013  hlimf  29014  hhssnv  29041  shscli  29094  shsval2i  29164  h1de2i  29330  fh3i  29400  fh4i  29401  cm2mi  29403  qlaxr3i  29413  mayetes3i  29506  ho0f  29528  hoif  29531  hodidi  29564  ho0subi  29572  hosd1i  29599  adjmo  29609  nmopsetn0  29642  nmfnsetn0  29655  funadj  29663  funcnvadj  29670  nmcexi  29803  cnlnadjlem8  29851  nmoptri2i  29876  opsqrlem4  29920  hmopidmchi  29928  pjoci  29957  pjinvari  29968  abrexdomjm  30267  elim2ifim  30300  iundisj2f  30340  rinvf1o  30375  dfcnv2  30422  snct  30449  fzodif2  30515  iundisj2fi  30520  dp2lt10  30560  dp2ltc  30563  dplti  30581  dpgti  30582  dpexpp1  30584  gsumle  30725  xrge0slmod  30917  xrge0pluscn  31183  zlmds  31205  zlmtset  31206  qqhre  31261  esumrnmpt2  31327  esumfsup  31329  esumpcvgval  31337  hasheuni  31344  esumcvg  31345  esumcvgsum  31347  esumsup  31348  esum2d  31352  dmsigagen  31403  ldgenpisyslem3  31424  measvuni  31473  voliune  31488  volfiniune  31489  br2base  31527  dya2iocuni  31541  eulerpartlem1  31625  eulerpartlemt  31629  eulerpartgbij  31630  fib0  31657  coinfliprv  31740  ballotlem2  31746  ballotlemic  31764  ballotlem7  31793  ballotth  31795  plymul02  31816  rpsqrtcn  31864  chtvalz  31900  circlemethnat  31912  circlevma  31913  circlemethhgt  31914  hgt750lem  31922  bnj226  32004  bnj1101  32056  bnj110  32130  bnj149  32147  bnj150  32148  bnj151  32149  bnj517  32157  bnj580  32185  bnj865  32195  bnj900  32201  bnj996  32228  bnj1110  32254  bnj1133  32261  bnj1128  32262  bnj1145  32265  bnj1137  32267  bnj1171  32272  bnj1176  32277  f1resfz0f1d  32361  subfacp1lem5  32431  subfacp1lem6  32432  kur14lem9  32461  cvmcov2  32522  cvmliftlem1  32532  cvmliftlem4  32535  cvmliftlem5  32536  gonanegoal  32599  satfv0  32605  satfv0fun  32618  fmlan0  32638  gonan0  32639  fmla0disjsuc  32645  ex-sategoelel12  32674  msrfo  32793  problem5  32912  brtpid1  32951  brtpid2  32952  brtpid3  32953  logi  32966  faclimlem1  32975  axextndbi  33049  poseq  33095  sltval2  33163  noxp1o  33170  nosepnelem  33184  txprel  33340  relsset  33349  relbigcup  33358  fvbigcup  33363  fnsingle  33380  fvsingle  33381  snelsingles  33383  funimage  33389  fullfunfnv  33407  imagesset  33414  funtransport  33492  colinrel  33518  funray  33601  funline  33603  0hf  33638  neibastop2lem  33708  filnetlem3  33728  nrmo  33758  waj-ax  33762  lukshef-ax2  33763  arg-ax  33764  limsucncmpi  33793  dnizeq0  33814  knoppcnlem8  33839  knoppcnlem11  33842  cnndvlem1  33876  bj-babylob  33938  bj-ax12ssb  33991  bj-nnfnth  34072  bj-disjcsn  34266  bj-snsetex  34278  bj-0eltag  34293  bj-2upln0  34338  bj-2upln1upl  34339  bj-isrvec  34578  f1omptsnlem  34620  f1omptsn  34621  icoreresf  34636  relowlssretop  34647  relowlpssretop  34648  domalom  34688  matunitlindf  34905  poimirlem3  34910  poimirlem9  34916  poimirlem16  34923  poimirlem17  34924  poimirlem18  34925  poimirlem19  34926  poimirlem20  34927  poimirlem26  34933  mblfinlem1  34944  mblfinlem2  34945  ismblfin  34948  voliunnfl  34951  cnambfre  34955  abrexdom  35020  fdc  35035  cncfres  35058  heibor1lem  35102  grposnOLD  35175  bicontr  35373  an12i  35391  tsim1  35423  ac6s6f  35466  vvdifopab  35536  brcnvrabga  35614  opabf  35635  xrnrel  35640  relcoels  35684  cnvcosseq  35697  refrelcoss3  35718  refrelcoss2  35719  symrelcoss2  35721  refrelcoss  35777  symrelcoss  35811  n0eldmqs  35898  ax13fromc9  36057  dedths  36113  renegclALT  36114  hlhilslem  39089  12gcd5e1  39124  60gcd7e1  39126  2xp3dxp2ge1d  39146  sn-axprlem3  39158  rtprmirr  39243  dffltz  39320  moxfr  39338  mapfzcons1  39363  diophrw  39405  0dioph  39424  vdioph  39425  rabren3dioph  39461  2nn0ind  39591  rpnnen3  39678  kelac2lem  39713  frlmpwfi  39747  ifpbiidcor2  39898  iscard4  39949  eliunov2  40073  xphe  40176  0he  40177  he0  40179  snhesn  40181  idhe  40182  frege54cor1c  40310  clsk1independent  40445  neicvgnvor  40515  amgm2d  40600  amgm3d  40601  amgm4d  40602  lhe4.4ex1a  40710  rusbcALT  40820  ipo0  40830  ifr0  40831  vk15.4j  40911  2sb5nd  40943  dfvd1ir  40956  dfvd2anir  40967  dfvd2ir  40969  dfvd3ir  40976  dfvd3anir  40979  iden2  40997  e0bir  41160  uun2221p1  41197  uun2221p2  41198  2sb5ndVD  41293  2sb5ndALT  41315  iunconnlem2  41318  fnchoice  41335  unisn0  41365  eliincex  41425  icof  41531  supminfxr  41789  fsumiunss  41905  climlimsupcex  42099  liminfltlimsupex  42111  liminflelimsupcex  42127  xlimrel  42150  xlimfun  42185  resincncf  42207  dvnprodlem3  42282  volioc  42306  volico  42317  dmvolss  42319  volioof  42321  stoweidlem13  42347  stoweidlem34  42368  stirlinglem5  42412  stirlinglem13  42420  stirlingr  42424  fourierdlem42  42483  fourierdlem62  42502  fouriersw  42565  etransc  42617  salexct  42666  salexct2  42671  salgencntex  42675  sge0rnn0  42699  gsumge0cl  42702  sge00  42707  sge0resplit  42737  sge0reuz  42778  omeiunle  42848  0ome  42860  icoresmbl  42874  ovn0lem  42896  ovnhoilem1  42932  hspmbl  42960  ovolval5lem3  42985  nsssmfmbf  43104  mbfpsssmf  43108  smfresal  43112  smfmullem4  43118  smfpimbor1lem1  43122  smfpimbor1lem2  43123  aistia  43182  aisfina  43183  aiffnbandciffatnotciffb  43189  axorbciffatcxorb  43190  abnotbtaxb  43200  abnotataxb  43201  eusnsn  43310  aiotaval  43342  aiota0ndef  43344  fundcmpsurinjimaid  43620  ichv  43658  ichf  43659  ichid  43660  ichcircshi  43661  icheq  43669  spr0nelg  43687  m3prm  43803  m7prm  43813  0noddALTV  43903  2noddALTV  43907  341fppr2  43948  9fppr8  43951  nfermltl8rev  43956  nfermltl2rev  43957  nfermltlrev  43958  sbgoldbo  44001  nnsum3primes4  44002  evengpop3  44012  oddinmgm  44131  nn0mnd  44135  2zrngamgm  44259  2zrngaabl  44264  2zrngmmgm  44266  2zrngnring  44272  fldhmsubc  44404  fldhmsubcALTV  44422  eliunxp2  44431  zlmodzxzldeplem  44602  zlmodzxzldep  44608  ldepslinc  44613  rrx2xpreen  44755  rrx2plordisom  44759  line2ylem  44787  line2  44788  line2x  44790  inlinecirc02plem  44822  ex-gte  44877  empty-surprise  44932  eximp-surprise2  44935  amgmw2d  44954