Theorem mpbir 234

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

Syntax hints:   ↔ 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:  pm5.74ri  275  con4bii  324  imnani  404  mpbir2an  711  imorri  854  orri  861  mpbir3an  1342  xorexmid  1524  tru  1546  had1  1609  nic-mpALT  1679  nic-ax  1680  nic-axALT  1681  nfi  1795  mpgbir  1806  nfxfr  1859  19.35ri  1886  ax5e  1919  ax6ev  1977  sbt  2076  equsb1v  2111  ax13  2376  ax13ALT  2426  moanmo  2626  axi12  2709  axbnd  2710  axexte  2712  axextmo  2715  nulmo  2716  vexw  2723  eqeltri  2830  nfcxfr  2898  neir  2938  neirr  2944  eqnetri  3005  nelir  3042  mprgbir  3069  cbvrexdva2  3360  issetri  3416  moeq  3611  rmoeq  3642  cdeqi  3669  eqsstri  3921  3sstr4i  3930  rmo0  4258  rabnc  4286  reuprg  4604  tpid1  4669  tpid2  4671  mosneq  4738  pwv  4803  uni0  4836  int0  4860  eqbrtri  5061  tr0  5157  trv  5158  zfrep4  5174  axnulALT  5182  0ex  5185  inex1  5195  elpwi2  5224  elpwi2OLD  5225  0elpw  5232  axpow2  5244  axpow3  5245  dvdemo1  5250  vpwex  5254  zfpair2  5307  exss  5331  brv  5340  opwo0id  5364  moop2  5369  pwundifOLD  5436  0sn0ep  5448  po0  5469  epse  5518  relxp  5553  rel0  5653  relopabiv  5674  relopabi  5676  relopabiALT  5677  eliunxp  5690  opeliunxp2  5691  dmi  5774  dmep  5776  domepOLD  5777  xpidtr  5966  xpima  6024  dmsn0  6051  cnvsn0  6052  0elon  6235  funmpt  6387  funmpt2  6388  funcnv0  6415  isarep2  6438  fresaunres2  6560  f0  6569  f10d  6663  f1o00  6664  f1oi  6667  f1osn  6669  brprcneu  6677  fvprc  6678  opabiotafun  6761  fvopab3ig  6783  opabex  7005  mptexgf  7007  eufnfv  7014  isof1oopb  7103  ncanth  7137  mpofun  7302  mpofunOLD  7303  reldmmpo  7312  ovid  7318  ovidig  7319  ovidi  7320  ovig  7323  ov3  7339  caovmo  7413  relmptopab  7423  porpss  7483  uniex2  7494  tfinds2  7609  finds  7641  finds2  7643  oprabex  7714  oprabex3  7715  f1stres  7750  f2ndres  7751  relmpoopab  7827  fsplitfpar  7852  opeliunxp2f  7917  tpos0  7963  wfrrel  8001  wfrlem14  8009  wfrlem16  8011  issmo  8026  tfrlem6  8059  tfrlem8  8061  tfrlem16  8070  tfr1a  8071  tfr1  8074  tz7.44lem1  8082  seqomlem2  8128  seqomlem3  8129  seqomlem4  8130  fnseqom  8132  0lt1o  8172  0we1  8174  eqer  8367  ecopover  8444  mapsnf1o3  8517  ssdomg  8613  en0  8630  ensn1  8632  snfi  8654  enrefnn  8657  xpcomf1o  8667  map2xp  8749  limensuci  8755  sdom1  8809  unblem4  8859  fidomdm  8886  marypha1lem  8982  hartogslem1  9091  hartogs  9093  card2on  9103  nelaneq  9148  epinid0  9149  ruALT  9152  elnanel  9155  cnvepnep  9156  inf2  9171  inf3lem6  9181  infeq5i  9184  zfinf2  9190  cantnflt  9220  cnfcom  9248  trcl  9255  tz9.1c  9257  tc2  9269  r1funlim  9280  r1fnon  9281  karden  9409  tskwe  9464  cardprclem  9493  pm54.43  9515  r0weon  9524  iunmapdisj  9535  alephfnon  9577  alephfplem4  9619  alephfp  9620  alephval3  9622  kmlem2  9663  dju1dif  9684  ackbij1  9750  ackbij2lem2  9752  ackbij2  9755  infpssrlem3  9817  hsmexlem4  9941  hsmexlem5  9942  ac2  9973  axac3  9976  ac6  9992  axdclem2  10032  dmct  10036  ondomon  10075  alephsucpw  10082  pwcfsdom  10095  cfpwsdom  10096  smobeth  10098  axpowndlem3  10111  zfcndun  10127  zfcndpow  10128  zfcndinf  10130  zfcndac  10131  wunex2  10250  uniwun  10252  wuncval2  10259  grur1  10332  axgroth5  10336  axgroth2  10337  axgroth6  10340  axgroth3  10343  grothtsk  10347  inaprc  10348  ltsopi  10400  dmaddpi  10402  dmmulpi  10403  1lt2pi  10417  nqerf  10442  addnqf  10460  mulnqf  10461  1lt2nq  10485  m1p1sr  10604  m1m1sr  10605  0lt1sr  10607  axaddf  10657  axmulf  10658  ax1cn  10661  subaddrii  11065  ixi  11359  recgt0ii  11636  nn1suc  11750  neg1lt0  11845  4d2e2  11898  arch  11985  un0mulcl  12022  pnf0xnn0  12067  3halfnz  12154  nummac  12236  indstr  12410  mnfltpnf  12616  ioof  12933  0nelfz1  13029  fzp1disj  13069  fzp1nel  13094  fzof  13138  om2uzrani  13423  om2uzf1oi  13424  uzrdglem  13428  uzrdgfni  13429  uzrdg0i  13430  ltwenn  13433  hashgf1o  13442  axdc4uzlem  13454  sq0  13659  irec  13668  facmapnn  13749  hashkf  13796  hashfxnn0  13801  hashf  13802  hash0  13832  prhash2ex  13864  hashsslei  13891  hashxplem  13898  hashbclem  13914  hashf1lem1  13918  hashf1lem1OLD  13919  s1dm  14063  eqs1  14067  ccat2s1p1  14086  cats1un  14184  revs1  14228  0csh0  14256  cshw1  14285  cats1fvn  14321  funcnvs1  14375  pfx2  14410  relexp0g  14483  relexpsucnnr  14486  rtrclreclem1  14518  dfrtrclrec2  14519  rtrclreclem2  14520  rtrclreclem4  14522  dfrtrcl2  14523  climmo  15016  fsumcom2  15234  ackbijnn  15288  incexclem  15296  infcvgaux1i  15317  fprodcom2  15442  bpolylem  15506  bpoly3  15516  bpoly4  15517  efcvgfsum  15543  cos1bnd  15644  cos2bnd  15645  znnen  15669  qnnen  15670  aleph1re  15702  3dvds  15788  n2dvdsm1  15826  divalglem5  15854  flodddiv4  15870  sadcaddlem  15912  sadadd2lem  15914  sadadd3  15916  sadaddlem  15921  lcmf0  16087  lcmfunsnlem2lem1  16091  lcmfunsnlem2  16093  coprmprod  16114  coprmproddvdslem  16115  2prm  16145  3lcm2e6  16184  phicl2  16217  pockthi  16355  unbenlem  16356  prmrec  16370  vdwlem13  16441  vdwnn  16446  ramcl2  16464  prmgapprmo  16510  mod2xnegi  16519  modsubi  16520  structcnvcnv  16612  setsres  16640  strfv  16646  strleun  16706  0rest  16818  firest  16821  restid  16822  prdsval  16843  prdsbas  16845  prdsplusg  16846  prdsmulr  16847  prdsvsca  16848  imasaddfnlem  16916  imasvscafn  16925  oppchomfval  17100  oppcbas  17104  2oppchomf  17110  rescbas  17216  rescco  17219  rescabs  17220  0ssc  17224  0subcat  17225  idfucl  17268  homarel  17420  dmaf  17433  cdaf  17434  setc2ohom  17479  catcfuccl  17497  relxpchom  17559  catcxpccl  17585  oppchofcl  17638  oyoncl  17648  odubas  17871  letsr  17965  mgmidmo  17998  efmndmgm  18178  smndex1ibas  18193  smndex1mgm  18200  smndex1mnd  18203  smndex2dbas  18207  smndex2dnrinv  18208  smndex2hbas  18209  pwmnd  18230  releqg  18457  ga0  18558  oppglem  18608  psgnunilem3  18754  psgnunilem4  18755  pmtrsn  18777  efgval  18973  efger  18974  efgsval2  18989  efgsp1  18993  efgsfo  18995  efgredleme  18999  efgredlem  19003  efgred  19004  cygctb  19143  gsum2d2lem  19224  gsum2d2  19225  gsumcom2  19226  dprd2d2  19297  pgpfaclem1  19334  mgplem  19375  mgpress  19381  opprlem  19512  reldvdsr  19528  00lsp  19884  sralem  20080  srasca  20084  sravsca  20085  cnfldfun  20241  cnfldfunALT  20242  xrsmgm  20264  zlmsca  20353  znbaslem  20369  resubdrg  20436  ocv0  20505  cssval  20510  thlbas  20524  thlle  20525  islinds2  20641  psrvscafval  20781  opsrbaslem  20872  psrbag0  20886  00ply1bas  21027  ply1plusgfvi  21029  matsca  21178  m2detleib  21394  tgdom  21741  tgidm  21743  indistps2ALT  21777  restbas  21921  resttopon  21924  rest0  21932  leordtval2  21975  iocpnfordt  21978  icomnfordt  21979  iooordt  21980  ist1-3  22112  1stcfb  22208  comppfsc  22295  1stckgen  22317  ptbasfi  22344  dfac14  22381  opnfbas  22605  hauspwpwf1  22750  alexsubALT  22814  ptcmplem5  22819  cnextrel  22826  ust0  22983  tuslem  23031  0met  23131  prdsdsf  23132  prdsxmetlem  23133  prdsmet  23135  setsmsbas  23240  setsmsds  23241  prdsbl  23256  tngds  23413  qtopbaslem  23523  xrtgioo  23570  xrsdsre  23574  zcld  23577  recld2  23578  reperflem  23582  retopconn  23593  iccpnfcnv  23708  bndth  23722  nmoleub2lem2  23880  zclmncvs  23912  recmet  24087  resscdrg  24122  ishl2  24134  recms  24144  volf  24293  iundisj2  24313  volsup  24320  icombl  24328  ioombl  24329  ismbf3d  24418  0plef  24436  0pledm  24437  itg1ge0  24450  mbfi1fseqlem5  24484  itg2addlem  24523  reldv  24634  limciun  24658  dvexp  24717  dveflem  24743  lhop1lem  24777  lhop  24780  elply2  24957  elplyd  24963  ply1term  24965  ply0  24969  plymullem  24977  qaa  25083  pserulm  25181  pserdvlem2  25187  efcn  25202  sincosq1lem  25254  tangtx  25262  sincos4thpi  25270  pigt3  25274  pige3ALT  25276  efif1olem4  25301  logf1o  25320  relogf1o  25322  log1  25341  loge  25342  relogiso  25353  dvrelog  25392  relogcn  25393  logcn  25402  cxpcn3  25501  resqrtcn  25502  2logb9irr  25545  leibpi  25692  log2ublem1  25696  birthday  25704  emcllem5  25749  harmonicbnd  25753  harmonicbnd2  25754  harmonicbnd3  25757  lgamgulm2  25785  lgamcvglem  25789  gamf  25792  ppiltx  25926  ppiublem1  25950  ppiub  25952  bclbnd  26028  bpos1lem  26030  bposlem8  26039  lgsquadlem2  26129  2sqlem9  26175  2sqlem10  26176  addsqnreup  26191  chebbnd1  26220  selberg2lem  26298  pntrsumo1  26313  selbergsb  26323  pntpbnd  26336  istrkg2ld  26418  tgcgr4  26489  ttgval  26833  ttglem  26834  cchhllem  26845  ax5seglem7  26893  axlowdimlem4  26903  axlowdimlem6  26905  axlowdimlem7  26906  axlowdimlem10  26909  axlowdimlem13  26912  axlowdimlem16  26915  uhgr0e  27028  uhgr0  27030  upgrbi  27050  umgrbi  27058  usgr0  27197  lfuhgr1v0e  27208  usgrexmpllem  27214  usgrexmpl  27217  griedg0prc  27218  cplgr0  27379  usgrexilem  27394  cffldtocusgr  27401  rgrusgrprc  27543  rusgrprc  27544  rgrprcx  27546  rgrx0ndm  27547  usgr2pthlem  27716  pthdlem2  27721  uspgrn2crct  27758  wwlksnext  27843  wwlksnfi  27856  disjxwwlkn  27863  clwwlknondisj  28060  0ewlk  28063  0wlk  28065  0pth  28074  1pthdlem1  28084  1trld  28091  wlk2v2elem2  28105  wlk2v2e  28106  upgr3v3e3cycl  28129  upgr4cycl4dv4e  28134  dfconngr1  28137  0conngr  28141  konigsbergumgr  28200  2wspmdisj  28286  2clwwlk2clwwlk  28299  numclwwlk3lem2lem  28332  numclwwlk3lem2  28333  ex-dif  28372  ex-in  28374  ex-eprel  28382  ex-id  28383  ex-fl  28396  ex-mod  28398  ex-hash  28402  ex-fpar  28411  avril1  28412  2bornot2b  28413  0vfval  28553  vsfval  28580  ajmoi  28805  ajfuni  28806  normlem2  29058  norm3adifii  29095  hhip  29124  hlim0  29182  hlimcaui  29183  hlimf  29184  hhssnv  29211  shscli  29264  shsval2i  29334  h1de2i  29500  fh3i  29570  fh4i  29571  cm2mi  29573  qlaxr3i  29583  mayetes3i  29676  ho0f  29698  hoif  29701  hodidi  29734  ho0subi  29742  hosd1i  29769  adjmo  29779  nmopsetn0  29812  nmfnsetn0  29825  funadj  29833  funcnvadj  29840  nmcexi  29973  cnlnadjlem8  30021  nmoptri2i  30046  opsqrlem4  30090  hmopidmchi  30098  pjoci  30127  pjinvari  30138  abrexdomjm  30438  elim2ifim  30474  iundisj2f  30515  rinvf1o  30551  dfcnv2  30600  snct  30635  fzodif2  30700  iundisj2fi  30705  dp2lt10  30745  dp2ltc  30748  dplti  30766  dpgti  30767  dpexpp1  30769  gsumle  30939  xrge0slmod  31132  zarcls  31408  zartopn  31409  xrge0pluscn  31474  zlmds  31496  zlmtset  31497  qqhre  31552  esumrnmpt2  31618  esumfsup  31620  esumpcvgval  31628  hasheuni  31635  esumcvg  31636  esumcvgsum  31638  esumsup  31639  esum2d  31643  dmsigagen  31694  ldgenpisyslem3  31715  measvuni  31764  voliune  31779  volfiniune  31780  br2base  31818  dya2iocuni  31832  eulerpartlem1  31916  eulerpartlemt  31920  eulerpartgbij  31921  fib0  31948  coinfliprv  32031  ballotlem2  32037  ballotlemic  32055  ballotlem7  32084  ballotth  32086  plymul02  32107  rpsqrtcn  32155  chtvalz  32191  circlemethnat  32203  circlevma  32204  circlemethhgt  32205  hgt750lem  32213  bnj226  32295  bnj1101  32347  bnj110  32421  bnj149  32438  bnj150  32439  bnj151  32440  bnj517  32448  bnj580  32476  bnj865  32486  bnj900  32492  bnj996  32519  bnj1110  32545  bnj1133  32552  bnj1128  32553  bnj1145  32556  bnj1137  32558  bnj1171  32563  bnj1176  32568  f1resfz0f1d  32655  subfacp1lem5  32729  subfacp1lem6  32730  kur14lem9  32759  cvmcov2  32820  cvmliftlem1  32830  cvmliftlem4  32833  cvmliftlem5  32834  gonanegoal  32897  satfv0  32903  satfv0fun  32916  fmlan0  32936  gonan0  32937  fmla0disjsuc  32943  ex-sategoelel12  32972  msrfo  33091  problem5  33210  brtpid1  33250  brtpid2  33251  brtpid3  33252  logi  33285  faclimlem1  33294  axextndbi  33366  poseq  33427  sltval2  33514  noxp1o  33521  nosepnelem  33537  noetasuplem2  33592  noetainflem2  33596  0slt1s  33678  txprel  33836  relsset  33845  relbigcup  33854  fvbigcup  33859  fnsingle  33876  fvsingle  33877  snelsingles  33879  funimage  33885  fullfunfnv  33903  imagesset  33910  funtransport  33988  colinrel  34014  funray  34097  funline  34099  0hf  34134  neibastop2lem  34204  filnetlem3  34224  nrmo  34254  waj-ax  34258  lukshef-ax2  34259  arg-ax  34260  limsucncmpi  34289  dnizeq0  34310  knoppcnlem8  34335  knoppcnlem11  34338  cnndvlem1  34372  bj-babylob  34441  bj-ax12ssb  34494  bj-nnfnth  34580  bj-disjcsn  34796  bj-snsetex  34808  bj-0eltag  34823  bj-2upln0  34868  bj-2upln1upl  34869  bj-isrvec  35117  f1omptsnlem  35162  f1omptsn  35163  icoreresf  35178  relowlssretop  35189  relowlpssretop  35190  domalom  35230  matunitlindf  35430  poimirlem3  35435  poimirlem9  35441  poimirlem16  35448  poimirlem17  35449  poimirlem18  35450  poimirlem19  35451  poimirlem20  35452  poimirlem26  35458  mblfinlem1  35469  mblfinlem2  35470  ismblfin  35473  voliunnfl  35476  cnambfre  35480  abrexdom  35543  fdc  35558  cncfres  35578  heibor1lem  35622  grposnOLD  35695  bicontr  35893  an12i  35911  tsim1  35943  ac6s6f  35986  vvdifopab  36054  brcnvrabga  36132  opabf  36153  xrnrel  36158  relcoels  36202  cnvcosseq  36215  refrelcoss3  36236  refrelcoss2  36237  symrelcoss2  36239  refrelcoss  36295  symrelcoss  36329  n0eldmqs  36416  ax13fromc9  36575  dedths  36631  renegclALT  36632  hlhilslem  39607  12gcd5e1  39663  60gcd7e1  39665  lcmineqlem23  39711  dvrelog2  39723  dvrelog3  39724  dvrelog2b  39725  aks4d1p1p6  39732  aks4d1p1p7  39733  aks4d1p1  39735  2xp3dxp2ge1d  39793  acos1half  39801  sn-axprlem3  39817  rtprmirr  39964  moxfr  40126  mapfzcons1  40151  diophrw  40193  0dioph  40212  vdioph  40213  rabren3dioph  40249  2nn0ind  40379  rpnnen3  40466  kelac2lem  40501  frlmpwfi  40535  ifpbiidcor2  40684  iscard4  40734  sqrtcval  40834  resqrtvalex  40838  eliunov2  40873  xphe  40975  0he  40976  he0  40978  snhesn  40980  idhe  40981  frege54cor1c  41109  clsk1independent  41242  neicvgnvor  41312  amgm2d  41396  amgm3d  41397  amgm4d  41398  lhe4.4ex1a  41525  rusbcALT  41635  ipo0  41645  ifr0  41646  vk15.4j  41726  2sb5nd  41758  dfvd1ir  41771  dfvd2anir  41782  dfvd2ir  41784  dfvd3ir  41791  dfvd3anir  41794  iden2  41812  e0bir  41975  uun2221p1  42012  uun2221p2  42013  2sb5ndVD  42108  2sb5ndALT  42130  iunconnlem2  42133  fnchoice  42150  unisn0  42180  eliincex  42238  icof  42337  supminfxr  42584  fsumiunss  42698  climlimsupcex  42892  liminfltlimsupex  42904  liminflelimsupcex  42920  xlimrel  42943  xlimfun  42978  resincncf  42998  dvnprodlem3  43071  volioc  43095  volico  43106  dmvolss  43108  volioof  43110  stoweidlem13  43136  stoweidlem34  43157  stirlinglem5  43201  stirlinglem13  43209  stirlingr  43213  fourierdlem42  43272  fourierdlem62  43291  fouriersw  43354  etransc  43406  salexct  43455  salexct2  43460  salgencntex  43464  sge0rnn0  43488  gsumge0cl  43491  sge00  43496  sge0resplit  43526  sge0reuz  43567  omeiunle  43637  0ome  43649  icoresmbl  43663  ovn0lem  43685  ovnhoilem1  43721  hspmbl  43749  ovolval5lem3  43774  nsssmfmbf  43893  mbfpsssmf  43897  smfresal  43901  smfmullem4  43907  smfpimbor1lem1  43911  smfpimbor1lem2  43912  aistia  43971  aisfina  43972  aiffnbandciffatnotciffb  43978  axorbciffatcxorb  43979  abnotbtaxb  43989  abnotataxb  43990  eusnsn  44099  aiotaval  44166  aiota0ndef  44168  fundcmpsurinjimaid  44444  ichv  44482  ichf  44483  ichid  44484  icht  44485  ichcircshi  44487  icheq  44495  spr0nelg  44509  m3prm  44625  m7prm  44633  0noddALTV  44722  2noddALTV  44726  341fppr2  44767  9fppr8  44770  nfermltl8rev  44775  nfermltl2rev  44776  nfermltlrev  44777  sbgoldbo  44820  nnsum3primes4  44821  evengpop3  44831  oddinmgm  44950  nn0mnd  44954  2zrngamgm  45078  2zrngaabl  45083  2zrngmmgm  45085  2zrngnring  45091  fldhmsubc  45223  fldhmsubcALTV  45241  eliunxp2  45250  zlmodzxzldeplem  45420  zlmodzxzldep  45426  ldepslinc  45431  rrx2xpreen  45646  rrx2plordisom  45650  line2ylem  45678  line2  45679  line2x  45681  inlinecirc02plem  45713  mosn  45737  mof0  45742  mof0ALT  45744  f1omo  45758  prstcleval  45855  prstcocval  45857  ex-gte  45931  empty-surprise  45986  eximp-surprise2  45989  amgmw2d  46008