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  710  imorri  852  orri  859  mpbir3an  1338  xorexmid  1520  tru  1542  had1  1605  nic-mpALT  1674  nic-ax  1675  nic-axALT  1676  nfi  1790  mpgbir  1801  nfxfr  1854  19.35ri  1880  ax5e  1913  ax6ev  1972  sbt  2071  equsb1v  2109  ax13  2382  ax13ALT  2436  moanmo  2684  axi12  2768  axbnd  2769  axexte  2771  axextmo  2774  nulmo  2775  vexw  2782  eqeltri  2886  nfcxfr  2953  neir  2990  neirr  2996  eqnetri  3057  nelir  3094  mprgbir  3121  cbvrexdva2  3404  vexOLD  3445  issetri  3457  moeq  3646  rmoeq  3677  cdeqi  3704  eqsstri  3949  3sstr4i  3958  rmo0  4273  rabnc  4295  reuprg  4599  tpid1  4664  tpid2  4666  mosneq  4733  pwv  4797  uni0  4828  int0  4852  eqbrtri  5051  tr0  5147  trv  5148  zfrep4  5164  axnulALT  5172  0ex  5175  inex1  5185  elpwi2  5213  elpwi2OLD  5214  0elpw  5221  axpow2  5233  axpow3  5234  dvdemo1  5239  vpwex  5243  zfpair2  5296  exss  5320  brv  5329  opwo0id  5352  moop2  5357  pwundifOLD  5422  0sn0ep  5434  po0  5454  epse  5502  relxp  5537  rel0  5636  relopabiv  5657  relopabi  5658  relopabiALT  5659  eliunxp  5672  opeliunxp2  5673  dmi  5755  dmep  5757  domepOLD  5758  xpidtr  5949  xpima  6006  dmsn0  6033  cnvsn0  6034  0elon  6212  funmpt  6362  funmpt2  6363  funcnv0  6390  isarep2  6413  fresaunres2  6524  f0  6534  f10d  6623  f1o00  6624  f1oi  6627  f1osn  6629  brprcneu  6637  opabiotafun  6719  fvopab3ig  6741  opabex  6960  mptexgf  6962  eufnfv  6969  isof1oopb  7057  ncanth  7091  mpofun  7255  reldmmpo  7264  ovid  7270  ovidig  7271  ovidi  7272  ovig  7275  ov3  7291  caovmo  7365  relmptopab  7375  porpss  7433  uniex2  7444  tfinds2  7558  finds  7589  finds2  7591  oprabex  7659  oprabex3  7660  f1stres  7695  f2ndres  7696  relmpoopab  7772  fsplitfpar  7797  opeliunxp2f  7859  tpos0  7905  wfrrel  7943  wfrlem14  7951  wfrlem16  7953  issmo  7968  tfrlem6  8001  tfrlem8  8003  tfrlem16  8012  tfr1a  8013  tfr1  8016  tz7.44lem1  8024  seqomlem2  8070  seqomlem3  8071  seqomlem4  8072  fnseqom  8074  0lt1o  8112  0we1  8114  eqer  8307  ecopover  8384  mapsnf1o3  8442  ssdomg  8538  ensn1  8556  snfi  8577  xpcomf1o  8589  map2xp  8671  limensuci  8677  sdom1  8702  unblem4  8757  fidomdm  8785  marypha1lem  8881  hartogslem1  8990  hartogs  8992  card2on  9002  nelaneq  9047  epinid0  9048  ruALT  9051  elnanel  9054  cnvepnep  9055  inf2  9070  inf3lem6  9080  infeq5i  9083  zfinf2  9089  cantnflt  9119  cnfcom  9147  trcl  9154  tz9.1c  9156  tc2  9168  r1funlim  9179  r1fnon  9180  karden  9308  tskwe  9363  cardprclem  9392  pm54.43  9414  r0weon  9423  iunmapdisj  9434  alephfnon  9476  alephfplem4  9518  alephfp  9519  alephval3  9521  kmlem2  9562  dju1dif  9583  ackbij1  9649  ackbij2lem2  9651  ackbij2  9654  infpssrlem3  9716  hsmexlem4  9840  hsmexlem5  9841  ac2  9872  axac3  9875  ac6  9891  axdclem2  9931  dmct  9935  ondomon  9974  alephsucpw  9981  pwcfsdom  9994  cfpwsdom  9995  smobeth  9997  axpowndlem3  10010  zfcndun  10026  zfcndpow  10027  zfcndinf  10029  zfcndac  10030  wunex2  10149  uniwun  10151  wuncval2  10158  grur1  10231  axgroth5  10235  axgroth2  10236  axgroth6  10239  axgroth3  10242  grothtsk  10246  inaprc  10247  ltsopi  10299  dmaddpi  10301  dmmulpi  10302  1lt2pi  10316  nqerf  10341  addnqf  10359  mulnqf  10360  1lt2nq  10384  m1p1sr  10503  m1m1sr  10504  0lt1sr  10506  axaddf  10556  axmulf  10557  ax1cn  10560  subaddrii  10964  ixi  11258  recgt0ii  11535  nn1suc  11647  neg1lt0  11742  4d2e2  11795  arch  11882  un0mulcl  11919  pnf0xnn0  11962  3halfnz  12049  nummac  12131  indstr  12304  mnfltpnf  12509  ioof  12825  0nelfz1  12921  fzp1disj  12961  fzp1nel  12986  fzof  13030  om2uzrani  13315  om2uzf1oi  13316  uzrdglem  13320  uzrdgfni  13321  uzrdg0i  13322  ltwenn  13325  hashgf1o  13334  axdc4uzlem  13346  sq0  13551  irec  13560  facmapnn  13641  hashkf  13688  hashfxnn0  13693  hashf  13694  hash0  13724  prhash2ex  13756  hashsslei  13783  hashxplem  13790  hashbclem  13806  hashf1lem1  13809  s1dm  13953  eqs1  13957  ccat2s1p1  13976  cats1un  14074  revs1  14118  0csh0  14146  cshw1  14175  cats1fvn  14211  funcnvs1  14265  pfx2  14300  relexp0g  14373  relexpsucnnr  14376  rtrclreclem1  14408  dfrtrclrec2  14409  rtrclreclem2  14410  rtrclreclem4  14412  dfrtrcl2  14413  climmo  14906  fsumcom2  15121  ackbijnn  15175  incexclem  15183  infcvgaux1i  15204  fprodcom2  15330  bpolylem  15394  bpoly3  15404  bpoly4  15405  efcvgfsum  15431  cos1bnd  15532  cos2bnd  15533  znnen  15557  qnnen  15558  aleph1re  15590  3dvds  15672  n2dvdsm1  15710  divalglem5  15738  flodddiv4  15754  sadcaddlem  15796  sadadd2lem  15798  sadadd3  15800  sadaddlem  15805  lcmf0  15968  lcmfunsnlem2lem1  15972  lcmfunsnlem2  15974  coprmprod  15995  coprmproddvdslem  15996  2prm  16026  3lcm2e6  16062  phicl2  16095  pockthi  16233  unbenlem  16234  prmrec  16248  vdwlem13  16319  vdwnn  16324  ramcl2  16342  prmgapprmo  16388  mod2xnegi  16397  modsubi  16398  structcnvcnv  16489  setsres  16517  strfv  16523  strleun  16583  0rest  16695  firest  16698  restid  16699  prdsval  16720  prdsbas  16722  prdsplusg  16723  prdsmulr  16724  prdsvsca  16725  imasaddfnlem  16793  imasvscafn  16802  oppchomfval  16976  oppcbas  16980  2oppchomf  16986  rescbas  17091  rescco  17094  rescabs  17095  0ssc  17099  0subcat  17100  idfucl  17143  homarel  17288  dmaf  17301  cdaf  17302  catcfuccl  17361  relxpchom  17423  catcxpccl  17449  oppchofcl  17502  oyoncl  17512  odubas  17735  letsr  17829  mgmidmo  17862  efmndmgm  18042  smndex1ibas  18057  smndex1mgm  18064  smndex1mnd  18067  smndex2dbas  18071  smndex2dnrinv  18072  smndex2hbas  18073  pwmnd  18094  releqg  18319  ga0  18420  oppglem  18470  psgnunilem3  18616  psgnunilem4  18617  pmtrsn  18639  efgval  18835  efger  18836  efgsval2  18851  efgsp1  18855  efgsfo  18857  efgredleme  18861  efgredlem  18865  efgred  18866  cygctb  19005  gsum2d2lem  19086  gsum2d2  19087  gsumcom2  19088  dprd2d2  19159  pgpfaclem1  19196  mgplem  19237  mgpress  19243  opprlem  19374  reldvdsr  19390  00lsp  19746  sralem  19942  srasca  19946  sravsca  19947  cnfldfun  20103  cnfldfunALT  20104  xrsmgm  20126  zlmsca  20214  znbaslem  20230  resubdrg  20297  ocv0  20366  cssval  20371  thlbas  20385  thlle  20386  islinds2  20502  psrvscafval  20628  opsrbaslem  20717  psrbag0  20733  00ply1bas  20869  ply1plusgfvi  20871  matsca  21020  m2detleib  21236  tgdom  21583  tgidm  21585  indistps2ALT  21619  restbas  21763  resttopon  21766  rest0  21774  leordtval2  21817  iocpnfordt  21820  icomnfordt  21821  iooordt  21822  ist1-3  21954  1stcfb  22050  comppfsc  22137  1stckgen  22159  ptbasfi  22186  dfac14  22223  opnfbas  22447  hauspwpwf1  22592  alexsubALT  22656  ptcmplem5  22661  cnextrel  22668  ust0  22825  tuslem  22873  0met  22973  prdsdsf  22974  prdsxmetlem  22975  prdsmet  22977  setsmsbas  23082  setsmsds  23083  prdsbl  23098  tngds  23254  qtopbaslem  23364  xrtgioo  23411  xrsdsre  23415  zcld  23418  recld2  23419  reperflem  23423  retopconn  23434  iccpnfcnv  23549  bndth  23563  nmoleub2lem2  23721  zclmncvs  23753  recmet  23927  resscdrg  23962  ishl2  23974  recms  23984  volf  24133  iundisj2  24153  volsup  24160  icombl  24168  ioombl  24169  ismbf3d  24258  0plef  24276  0pledm  24277  itg1ge0  24290  mbfi1fseqlem5  24323  itg2addlem  24362  reldv  24473  limciun  24497  dvexp  24556  dveflem  24582  lhop1lem  24616  lhop  24619  elply2  24793  elplyd  24799  ply1term  24801  ply0  24805  plymullem  24813  qaa  24919  pserulm  25017  pserdvlem2  25023  efcn  25038  sincosq1lem  25090  tangtx  25098  sincos4thpi  25106  pigt3  25110  pige3ALT  25112  efif1olem4  25137  logf1o  25156  relogf1o  25158  log1  25177  loge  25178  relogiso  25189  dvrelog  25228  relogcn  25229  logcn  25238  cxpcn3  25337  resqrtcn  25338  2logb9irr  25381  leibpi  25528  log2ublem1  25532  birthday  25540  emcllem5  25585  harmonicbnd  25589  harmonicbnd2  25590  harmonicbnd3  25593  lgamgulm2  25621  lgamcvglem  25625  gamf  25628  ppiltx  25762  ppiublem1  25786  ppiub  25788  bclbnd  25864  bpos1lem  25866  bposlem8  25875  lgsquadlem2  25965  2sqlem9  26011  2sqlem10  26012  addsqnreup  26027  chebbnd1  26056  selberg2lem  26134  pntrsumo1  26149  selbergsb  26159  pntpbnd  26172  istrkg2ld  26254  tgcgr4  26325  ttgval  26669  ttglem  26670  cchhllem  26681  ax5seglem7  26729  axlowdimlem4  26739  axlowdimlem6  26741  axlowdimlem7  26742  axlowdimlem10  26745  axlowdimlem13  26748  axlowdimlem16  26751  uhgr0e  26864  uhgr0  26866  upgrbi  26886  umgrbi  26894  usgr0  27033  lfuhgr1v0e  27044  usgrexmpllem  27050  usgrexmpl  27053  griedg0prc  27054  cplgr0  27215  usgrexilem  27230  cffldtocusgr  27237  rgrusgrprc  27379  rusgrprc  27380  rgrprcx  27382  rgrx0ndm  27383  usgr2pthlem  27552  pthdlem2  27557  uspgrn2crct  27594  wwlksnext  27679  wwlksnfi  27692  disjxwwlkn  27699  clwwlknondisj  27896  0ewlk  27899  0wlk  27901  0pth  27910  1pthdlem1  27920  1trld  27927  wlk2v2elem2  27941  wlk2v2e  27942  upgr3v3e3cycl  27965  upgr4cycl4dv4e  27970  dfconngr1  27973  0conngr  27977  konigsbergumgr  28036  2wspmdisj  28122  2clwwlk2clwwlk  28135  numclwwlk3lem2lem  28168  numclwwlk3lem2  28169  ex-dif  28208  ex-in  28210  ex-eprel  28218  ex-id  28219  ex-fl  28232  ex-mod  28234  ex-hash  28238  ex-fpar  28247  avril1  28248  2bornot2b  28249  0vfval  28389  vsfval  28416  ajmoi  28641  ajfuni  28642  normlem2  28894  norm3adifii  28931  hhip  28960  hlim0  29018  hlimcaui  29019  hlimf  29020  hhssnv  29047  shscli  29100  shsval2i  29170  h1de2i  29336  fh3i  29406  fh4i  29407  cm2mi  29409  qlaxr3i  29419  mayetes3i  29512  ho0f  29534  hoif  29537  hodidi  29570  ho0subi  29578  hosd1i  29605  adjmo  29615  nmopsetn0  29648  nmfnsetn0  29661  funadj  29669  funcnvadj  29676  nmcexi  29809  cnlnadjlem8  29857  nmoptri2i  29882  opsqrlem4  29926  hmopidmchi  29934  pjoci  29963  pjinvari  29974  abrexdomjm  30275  elim2ifim  30312  iundisj2f  30353  rinvf1o  30389  dfcnv2  30439  snct  30475  fzodif2  30541  iundisj2fi  30546  dp2lt10  30586  dp2ltc  30589  dplti  30607  dpgti  30608  dpexpp1  30610  gsumle  30775  xrge0slmod  30968  zarcls  31227  zartopn  31228  xrge0pluscn  31293  zlmds  31315  zlmtset  31316  qqhre  31371  esumrnmpt2  31437  esumfsup  31439  esumpcvgval  31447  hasheuni  31454  esumcvg  31455  esumcvgsum  31457  esumsup  31458  esum2d  31462  dmsigagen  31513  ldgenpisyslem3  31534  measvuni  31583  voliune  31598  volfiniune  31599  br2base  31637  dya2iocuni  31651  eulerpartlem1  31735  eulerpartlemt  31739  eulerpartgbij  31740  fib0  31767  coinfliprv  31850  ballotlem2  31856  ballotlemic  31874  ballotlem7  31903  ballotth  31905  plymul02  31926  rpsqrtcn  31974  chtvalz  32010  circlemethnat  32022  circlevma  32023  circlemethhgt  32024  hgt750lem  32032  bnj226  32114  bnj1101  32166  bnj110  32240  bnj149  32257  bnj150  32258  bnj151  32259  bnj517  32267  bnj580  32295  bnj865  32305  bnj900  32311  bnj996  32338  bnj1110  32364  bnj1133  32371  bnj1128  32372  bnj1145  32375  bnj1137  32377  bnj1171  32382  bnj1176  32387  f1resfz0f1d  32471  subfacp1lem5  32544  subfacp1lem6  32545  kur14lem9  32574  cvmcov2  32635  cvmliftlem1  32645  cvmliftlem4  32648  cvmliftlem5  32649  gonanegoal  32712  satfv0  32718  satfv0fun  32731  fmlan0  32751  gonan0  32752  fmla0disjsuc  32758  ex-sategoelel12  32787  msrfo  32906  problem5  33025  brtpid1  33064  brtpid2  33065  brtpid3  33066  logi  33079  faclimlem1  33088  axextndbi  33162  poseq  33208  sltval2  33276  noxp1o  33283  nosepnelem  33297  txprel  33453  relsset  33462  relbigcup  33471  fvbigcup  33476  fnsingle  33493  fvsingle  33494  snelsingles  33496  funimage  33502  fullfunfnv  33520  imagesset  33527  funtransport  33605  colinrel  33631  funray  33714  funline  33716  0hf  33751  neibastop2lem  33821  filnetlem3  33841  nrmo  33871  waj-ax  33875  lukshef-ax2  33876  arg-ax  33877  limsucncmpi  33906  dnizeq0  33927  knoppcnlem8  33952  knoppcnlem11  33955  cnndvlem1  33989  bj-babylob  34051  bj-ax12ssb  34104  bj-nnfnth  34187  bj-disjcsn  34387  bj-snsetex  34399  bj-0eltag  34414  bj-2upln0  34459  bj-2upln1upl  34460  bj-isrvec  34708  f1omptsnlem  34753  f1omptsn  34754  icoreresf  34769  relowlssretop  34780  relowlpssretop  34781  domalom  34821  matunitlindf  35055  poimirlem3  35060  poimirlem9  35066  poimirlem16  35073  poimirlem17  35074  poimirlem18  35075  poimirlem19  35076  poimirlem20  35077  poimirlem26  35083  mblfinlem1  35094  mblfinlem2  35095  ismblfin  35098  voliunnfl  35101  cnambfre  35105  abrexdom  35168  fdc  35183  cncfres  35203  heibor1lem  35247  grposnOLD  35320  bicontr  35518  an12i  35536  tsim1  35568  ac6s6f  35611  vvdifopab  35681  brcnvrabga  35759  opabf  35780  xrnrel  35785  relcoels  35829  cnvcosseq  35842  refrelcoss3  35863  refrelcoss2  35864  symrelcoss2  35866  refrelcoss  35922  symrelcoss  35956  n0eldmqs  36043  ax13fromc9  36202  dedths  36258  renegclALT  36259  hlhilslem  39234  12gcd5e1  39291  60gcd7e1  39293  lcmineqlem23  39339  3lexlogpow5ineq1  39341  3lexlogpow5ineq2  39342  2xp3dxp2ge1d  39387  sn-axprlem3  39401  rtprmirr  39502  dffltz  39615  moxfr  39633  mapfzcons1  39658  diophrw  39700  0dioph  39719  vdioph  39720  rabren3dioph  39756  2nn0ind  39886  rpnnen3  39973  kelac2lem  40008  frlmpwfi  40042  ifpbiidcor2  40191  iscard4  40241  sqrtcval  40341  resqrtvalex  40345  eliunov2  40380  xphe  40482  0he  40483  he0  40485  snhesn  40487  idhe  40488  frege54cor1c  40616  clsk1independent  40749  neicvgnvor  40819  amgm2d  40904  amgm3d  40905  amgm4d  40906  lhe4.4ex1a  41033  rusbcALT  41143  ipo0  41153  ifr0  41154  vk15.4j  41234  2sb5nd  41266  dfvd1ir  41279  dfvd2anir  41290  dfvd2ir  41292  dfvd3ir  41299  dfvd3anir  41302  iden2  41320  e0bir  41483  uun2221p1  41520  uun2221p2  41521  2sb5ndVD  41616  2sb5ndALT  41638  iunconnlem2  41641  fnchoice  41658  unisn0  41688  eliincex  41746  icof  41848  supminfxr  42103  fsumiunss  42217  climlimsupcex  42411  liminfltlimsupex  42423  liminflelimsupcex  42439  xlimrel  42462  xlimfun  42497  resincncf  42517  dvnprodlem3  42590  volioc  42614  volico  42625  dmvolss  42627  volioof  42629  stoweidlem13  42655  stoweidlem34  42676  stirlinglem5  42720  stirlinglem13  42728  stirlingr  42732  fourierdlem42  42791  fourierdlem62  42810  fouriersw  42873  etransc  42925  salexct  42974  salexct2  42979  salgencntex  42983  sge0rnn0  43007  gsumge0cl  43010  sge00  43015  sge0resplit  43045  sge0reuz  43086  omeiunle  43156  0ome  43168  icoresmbl  43182  ovn0lem  43204  ovnhoilem1  43240  hspmbl  43268  ovolval5lem3  43293  nsssmfmbf  43412  mbfpsssmf  43416  smfresal  43420  smfmullem4  43426  smfpimbor1lem1  43430  smfpimbor1lem2  43431  aistia  43490  aisfina  43491  aiffnbandciffatnotciffb  43497  axorbciffatcxorb  43498  abnotbtaxb  43508  abnotataxb  43509  eusnsn  43618  aiotaval  43650  aiota0ndef  43652  fundcmpsurinjimaid  43928  ichv  43966  ichf  43967  ichid  43968  icht  43969  ichcircshi  43971  icheq  43979  spr0nelg  43993  m3prm  44109  m7prm  44117  0noddALTV  44207  2noddALTV  44211  341fppr2  44252  9fppr8  44255  nfermltl8rev  44260  nfermltl2rev  44261  nfermltlrev  44262  sbgoldbo  44305  nnsum3primes4  44306  evengpop3  44316  oddinmgm  44435  nn0mnd  44439  2zrngamgm  44563  2zrngaabl  44568  2zrngmmgm  44570  2zrngnring  44576  fldhmsubc  44708  fldhmsubcALTV  44726  eliunxp2  44735  zlmodzxzldeplem  44907  zlmodzxzldep  44913  ldepslinc  44918  rrx2xpreen  45133  rrx2plordisom  45137  line2ylem  45165  line2  45166  line2x  45168  inlinecirc02plem  45200  ex-gte  45255  empty-surprise  45310  eximp-surprise2  45313  amgmw2d  45332