Theorem mpbir 221

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

Syntax hints:   ↔ wb 196

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 197

This theorem is referenced by:  pm5.74ri  261  con4bii  311  orri  391  imorri  430  imnani  439  mpbir2an  955  mpbir3an  1244  xorexmid  1480  tru  1487  had1  1542  nic-mpALT  1597  nic-ax  1598  nic-axALT  1599  nfi  1714  mpgbir  1726  nfxfr  1779  19.35ri  1807  nfxfrOLD  1837  ax5e  1841  ax6ev  1890  exanOLDOLD  2169  ax13  2249  ax13ALT  2305  euequ1  2476  moanmo  2532  axi12  2600  axext2  2603  eqeltri  2697  nfcxfr  2762  neir  2797  neirr  2803  eqnetri  2864  nelir  2900  mprgbir  2927  vex  3203  issetri  3210  moeq  3382  rmoeq  3405  cdeqi  3420  eqsstri  3635  3sstr4i  3644  rabnc  3962  tpid1  4303  tpid2  4304  pwv  4433  uni0  4465  int0  4490  eqbrtri  4674  tr0  4764  trv  4765  zfrep4  4779  zfnuleu  4786  axnulALT  4787  0ex  4790  inex1  4799  elpwi2  4829  0elpw  4834  axpow2  4845  axpow3  4846  pwex  4848  dvdemo1  4902  zfpair2  4907  exss  4931  brv  4941  opwo0id  4961  moop2  4966  pwundif  5021  po0  5050  epse  5097  relsnop  5224  relxp  5227  rel0  5243  relopabi  5245  relopabiALT  5246  eliunxp  5259  opeliunxp2  5260  dmi  5340  xpidtr  5518  xpima  5576  cnvcnv  5586  cnvcnvOLD  5587  dmsn0  5602  cnvsn0  5603  0elon  5778  funmpt  5926  funmpt2  5927  funcnv0  5955  isarep2  5978  fresaunres2  6076  f0  6086  f10  6169  f10d  6170  f1o00  6171  f1oi  6174  f1osn  6176  brprcneu  6184  opabiotafun  6259  fvopab3ig  6278  opabex  6483  mptexgf  6485  eufnfv  6491  isof1oopb  6575  canth  6608  ncanth  6609  mpt2fun  6762  reldmmpt2  6771  ovid  6777  ovidig  6778  ovidi  6779  ovig  6782  ov3  6797  caovmo  6871  relmptopab  6883  porpss  6941  uniex2  6952  snnexOLD  6967  tfinds2  7063  finds  7092  finds2  7094  oprabex  7156  oprabex3  7157  f1stres  7190  f2ndres  7191  relmpt2opab  7259  opeliunxp2f  7336  tpos0  7382  wfrrel  7420  wfrlem14  7428  wfrlem16  7430  issmo  7445  tfrlem6  7478  tfrlem8  7480  tfrlem16  7489  tfr1a  7490  tfr1  7493  tz7.44lem1  7501  seqomlem2  7546  seqomlem3  7547  seqomlem4  7548  fnseqom  7550  0lt1o  7584  0we1  7586  eqer  7777  eqerOLD  7778  ecopover  7851  ecopoverOLD  7852  mapsnf1o3  7906  ssdomg  8001  ensn1  8020  snfi  8038  xpcomf1o  8049  map2xp  8130  limensuci  8136  sdom1  8160  unblem4  8215  fidomdm  8243  marypha1lem  8339  hartogslem1  8447  hartogs  8449  card2on  8459  ruALT  8508  inf2  8520  inf3lem6  8530  infeq5i  8533  zfinf2  8539  cantnflt  8569  cnfcom  8597  trcl  8604  tz9.1c  8606  tc2  8618  r1funlim  8629  r1fnon  8630  karden  8758  tskwe  8776  cardprclem  8805  pm54.43  8826  r0weon  8835  iunmapdisj  8846  alephfnon  8888  alephfplem4  8930  alephfp  8931  alephval3  8933  aceq3lem  8943  kmlem2  8973  cda1dif  8998  ackbij1  9060  ackbij2lem2  9062  ackbij2  9065  infpssrlem3  9127  hsmexlem4  9251  hsmexlem5  9252  axdc3lem4  9275  ac2  9283  axac3  9286  ac6  9302  axdclem2  9342  dmct  9346  ondomon  9385  alephsucpw  9392  pwcfsdom  9405  cfpwsdom  9406  smobeth  9408  axpowndlem3  9421  zfcndun  9437  zfcndpow  9438  zfcndinf  9440  zfcndac  9441  wunex2  9560  uniwun  9562  wuncval2  9569  grur1  9642  axgroth5  9646  axgroth2  9647  axgroth6  9650  axgroth3  9653  grothtsk  9657  inaprc  9658  ltsopi  9710  dmaddpi  9712  dmmulpi  9713  1lt2pi  9727  nqerf  9752  addnqf  9770  mulnqf  9771  1lt2nq  9795  m1p1sr  9913  m1m1sr  9914  0lt1sr  9916  axaddf  9966  axmulf  9967  ax1cn  9970  subaddrii  10370  ixi  10656  recgt0ii  10929  nn1suc  11041  neg1lt0  11127  4d2e2  11184  arch  11289  un0mulcl  11327  pnf0xnn0  11370  3halfnz  11456  nummac  11558  uzf  11690  indstr  11756  mnfltpnf  11960  ixxf  12185  ioof  12271  fzf  12330  0nelfz1  12360  fzp1disj  12399  fzp1nel  12424  fzof  12467  om2uzrani  12751  om2uzf1oi  12752  uzrdglem  12756  uzrdgfni  12757  uzrdg0i  12758  ltwenn  12761  hashgf1o  12770  axdc4uzlem  12782  sq0  12955  irec  12964  facmapnn  13072  hashkf  13119  hashfxnn0  13124  hashf  13125  hashfOLD  13126  hash0  13158  prhash2ex  13187  hashsslei  13213  hashxplem  13220  hashbclem  13236  hashf1lem1  13239  wrdexg  13315  s1dm  13388  revs1  13514  0csh0  13539  cshw1  13568  cats1fvn  13603  s2dm  13635  funcnvs1  13657  relexp0g  13762  relexpsucnnr  13765  dfrtrclrec2  13797  rtrclreclem1  13798  rtrclreclem2  13799  rtrclreclem4  13801  dfrtrcl2  13802  climmo  14288  fsumcom2  14505  fsumcom2OLD  14506  ackbijnn  14560  incexclem  14568  infcvgaux1i  14589  fprodcom2  14714  fprodcom2OLD  14715  fprodn0f  14722  fprodge0  14724  fprodge1  14726  bpolylem  14779  bpoly3  14789  bpoly4  14790  efcvgfsum  14816  cos1bnd  14917  cos2bnd  14918  znnen  14941  qnnen  14942  aleph1re  14974  3dvds  15052  3dvdsOLD  15053  n2dvdsm1  15105  n2dvds3  15107  divalglem5  15120  flodddiv4  15137  bitsf  15149  sadcaddlem  15179  sadadd2lem  15181  sadadd3  15183  sadaddlem  15188  lcmf0  15347  lcmfunsnlem2lem1  15351  lcmfunsnlem2  15353  coprmprod  15375  coprmproddvdslem  15376  2prm  15405  3lcm2e6  15440  phicl2  15473  pockthi  15611  unbenlem  15612  prmrec  15626  vdwlem13  15697  vdwnn  15702  ramcl2  15720  prmgapprmo  15766  mod2xnegi  15775  modsubi  15776  prmo4  15835  prmo5  15836  prmo6  15837  structcnvcnv  15871  setsres  15901  strfv  15907  strlemor1OLD  15969  strleun  15972  0rest  16090  firest  16093  restid  16094  prdsval  16115  prdsbas  16117  prdsplusg  16118  prdsmulr  16119  prdsvsca  16120  prdsds  16124  imasaddfnlem  16188  imasvscafn  16197  oppchomfval  16374  oppcbas  16378  2oppchomf  16384  rescbas  16489  rescco  16492  rescabs  16493  0ssc  16497  0subcat  16498  idfucl  16541  wunnat  16616  homarel  16686  dmaf  16699  cdaf  16700  catcfuccl  16759  relxpchom  16821  catcxpccl  16847  oppchofcl  16900  oyoncl  16910  odubas  17133  letsr  17227  mgmidmo  17259  releqg  17641  ga0  17731  oppglem  17780  psgnunilem3  17916  psgnunilem4  17917  pmtrsn  17939  efgval  18130  efger  18131  efgsp1  18150  efgsfo  18152  efgredleme  18156  efgredlem  18160  efgred  18161  cygctb  18293  gsum2d2lem  18372  gsum2d2  18373  gsumcom2  18374  dprd2d2  18443  pgpfaclem1  18480  mgplem  18494  mgpress  18500  opprlem  18628  reldvdsr  18644  00lsp  18981  sralem  19177  srasca  19181  sravsca  19182  psrvscafval  19390  opsrbaslem  19477  opsrbaslemOLD  19478  psrbag0  19494  00ply1bas  19610  ply1plusgfvi  19612  cnfldfun  19758  cnfldfunALT  19759  xrsmgm  19781  zlmsca  19869  znbaslem  19886  znbaslemOLD  19887  resubdrg  19954  ocvfval  20010  ocv0  20021  cssval  20026  thlbas  20040  thlle  20041  islinds2  20152  matsca  20221  m2detleib  20437  tgdom  20782  tgidm  20784  indistps2ALT  20818  restbas  20962  resttopon  20965  rest0  20973  leordtval2  21016  iocpnfordt  21019  icomnfordt  21020  iooordt  21021  cnpfval  21038  iscnp2  21043  ist1-3  21153  1stcfb  21248  islly2  21287  comppfsc  21335  1stckgen  21357  ptbasfi  21384  xkotf  21388  dfac14  21421  opnfbas  21646  hauspwpwf1  21791  alexsubALTlem4  21854  alexsubALT  21855  ptcmplem5  21860  cnextrel  21867  ust0  22023  tuslem  22071  0met  22171  prdsdsf  22172  prdsxmetlem  22173  prdsmet  22175  setsmsbas  22280  setsmsds  22281  prdsbl  22296  tngds  22452  qtopbaslem  22562  xrtgioo  22609  xrsdsre  22613  zcld  22616  recld2  22617  sszcld  22620  reperflem  22621  retopconn  22632  iccpnfcnv  22743  bndth  22757  ishtpy  22771  nmoleub2lem2  22916  zclmncvs  22948  recmet  23120  resscdrg  23154  ishl2  23166  recms  23168  volf  23297  iundisj2  23317  volsup  23324  icombl  23332  ioombl  23333  ismbf3d  23421  0plef  23439  0pledm  23440  itg1ge0  23453  mbfi1fseqlem5  23486  itg2addlem  23525  iblcnlem1  23554  reldv  23634  limciun  23658  dvexp  23716  dveflem  23742  lhop1lem  23776  lhop  23779  elply2  23952  elplyd  23958  ply1term  23960  ply0  23964  plymullem  23972  qaa  24078  pserulm  24176  pserdvlem2  24182  efcn  24197  sincosq1lem  24249  tangtx  24257  sincos4thpi  24265  sincos6thpi  24267  pige3  24269  efif1olem4  24291  logf1o  24311  relogf1o  24313  log1  24332  loge  24333  relogiso  24344  dvrelog  24383  relogcn  24384  logcn  24393  cxpcn3  24489  resqrtcn  24490  leibpi  24669  log2ublem1  24673  birthday  24681  emcllem5  24726  harmonicbnd  24730  harmonicbnd2  24731  emgt0  24733  harmonicbnd3  24734  lgamgulm2  24762  lgamcvglem  24766  gamf  24769  ppiltx  24903  ppiublem1  24927  ppiub  24929  bclbnd  25005  bpos1lem  25007  bposlem8  25016  lgsquadlem2  25106  2sqlem9  25152  2sqlem10  25153  chebbnd1  25161  selberg2lem  25239  pntrsumo1  25254  selbergsb  25264  pntpbnd  25277  istrkg2ld  25359  tgcgr4  25426  ttgval  25755  ttglem  25756  cchhllem  25767  ax5seglem7  25815  axlowdimlem4  25825  axlowdimlem6  25827  axlowdimlem7  25828  axlowdimlem10  25831  axlowdimlem13  25834  axlowdimlem16  25837  uhgr0e  25966  uhgr0  25968  upgrbi  25988  umgrbi  25996  usgr0  26135  lfuhgr1v0e  26146  usgrexmpllem  26152  usgrexmpl  26155  griedg0prc  26156  cplgr0  26321  usgrexilem  26336  cffldtocusgr  26343  rgrusgrprc  26485  rusgrprc  26486  rgrprcx  26488  rgrx0ndm  26489  usgr2pthlem  26659  pthdlem2  26664  uspgrn2crct  26700  wwlksnext  26788  wwlksnfi  26801  disjxwwlkn  26808  clwwlksndisj  26973  0ewlk  26975  0wlk  26977  0pth  26986  1pthdlem1  26995  1trld  27002  wlk2v2elem2  27016  wlk2v2e  27017  upgr3v3e3cycl  27040  upgr4cycl4dv4e  27045  dfconngr1  27048  0conngr  27052  konigsbergumgr  27112  konigsbergupgrOLD  27113  2wspmdisj  27201  numclwwlk3lem  27241  ex-dif  27280  ex-in  27282  ex-eprel  27290  ex-id  27291  ex-fl  27304  ex-mod  27306  ex-hash  27310  avril1  27319  2bornot2b  27320  0vfval  27461  vsfval  27488  ajmoi  27714  ajfuni  27715  normlem2  27968  norm3adifii  28005  hhip  28034  hlim0  28092  hlimcaui  28093  hlimf  28094  hhssnv  28121  shscli  28176  shsval2i  28246  h1de2i  28412  fh3i  28482  fh4i  28483  cm2mi  28485  qlaxr3i  28495  mayetes3i  28588  ho0f  28610  hoif  28613  hodidi  28646  ho0subi  28654  hosd1i  28681  adjmo  28691  nmopsetn0  28724  nmfnsetn0  28737  funadj  28745  funcnvadj  28752  nmcexi  28885  cnlnadjlem8  28933  nmoptri2i  28958  opsqrlem4  29002  hmopidmchi  29010  pjoci  29039  pjinvari  29050  abrexdomjm  29345  elim2ifim  29364  iundisj2f  29403  rinvf1o  29432  funcnvmptOLD  29467  dfcnv2  29476  snct  29491  fpwrelmap  29508  fzodif2  29552  iundisj2fi  29556  dp2lt10  29591  dp2ltc  29594  dplti  29613  dpgti  29614  dpexpp1  29616  gsumle  29779  xrge0slmod  29844  xrge0pluscn  29986  zlmds  30008  zlmtset  30009  qqhre  30064  esumrnmpt2  30130  esumfsup  30132  esumpcvgval  30140  hasheuni  30147  esumcvg  30148  esumcvgsum  30150  esumsup  30151  esum2d  30155  dmsigagen  30207  ldgenpisyslem3  30228  measvuni  30277  voliune  30292  volfiniune  30293  br2base  30331  dya2iocuni  30345  eulerpartlem1  30429  eulerpartlemt  30433  eulerpartgbij  30434  fib0  30461  coinfliprv  30544  ballotlem2  30550  ballotlemic  30568  ballotlem7  30597  ballotth  30599  plymul02  30623  rpsqrtcn  30671  chtvalz  30707  circlemethnat  30719  circlevma  30720  circlemethhgt  30721  hgt750lem  30729  bnj226  30802  bnj1101  30855  bnj110  30928  bnj149  30945  bnj150  30946  bnj151  30947  bnj517  30955  bnj580  30983  bnj865  30993  bnj900  30999  bnj996  31025  bnj1110  31050  bnj1133  31057  bnj1128  31058  bnj1145  31061  bnj1137  31063  bnj1171  31068  bnj1176  31073  subfacp1lem5  31166  subfacp1lem6  31167  kur14lem9  31196  cvmcov2  31257  cvmliftlem1  31267  cvmliftlem4  31270  cvmliftlem5  31271  msrfo  31443  problem5  31563  brtpid1  31602  brtpid2  31603  brtpid3  31604  logi  31620  faclimlem1  31629  domep  31698  axextndbi  31710  poseq  31750  frrlem10  31791  sltval2  31809  noxp1o  31816  nosepnelem  31830  txprel  31986  relsset  31995  relbigcup  32004  fvbigcup  32009  fnsingle  32026  fvsingle  32027  snelsingles  32029  funimage  32035  fullfunfnv  32053  imagesset  32060  funtransport  32138  colinrel  32164  funray  32247  funline  32249  0hf  32284  neibastop2lem  32355  filnetlem3  32375  waj-ax  32413  lukshef-ax2  32414  arg-ax  32415  limsucncmpi  32444  dnizeq0  32465  knoppcnlem8  32490  knoppcnlem11  32493  cnndvlem1  32528  bj-babylob  32589  bj-ax12ssb  32635  bj-dvdemo1  32802  bj-disjcsn  32936  bj-snsetex  32951  bj-0eltag  32966  bj-2upln0  33011  bj-2upln1upl  33012  f1omptsnlem  33183  f1omptsn  33184  icoreresf  33200  relowlssretop  33211  relowlpssretop  33212  pigt3  33402  matunitlindf  33407  poimirlem3  33412  poimirlem9  33418  poimirlem16  33425  poimirlem17  33426  poimirlem18  33427  poimirlem19  33428  poimirlem20  33429  poimirlem26  33435  mblfinlem1  33446  mblfinlem2  33447  ismblfin  33450  voliunnfl  33453  cnambfre  33458  cover2  33508  abrexdom  33525  fdc  33541  cncfres  33564  heibor1lem  33608  grposnOLD  33681  bicontr  33879  an12i  33900  tsim1  33937  ac6s6f  33981  vvdifopab  34024  xrnrel  34136  ax13fromc9  34191  dedths  34248  renegclALT  34249  hlhilslem  37230  moxfr  37255  mapfzcons1  37280  diophrw  37322  0dioph  37342  vdioph  37343  rabren3dioph  37379  2nn0ind  37510  rpnnen3  37599  kelac2lem  37634  frlmpwfi  37668  ifpbiidcor2  37828  relintabex  37887  eliunov2  37971  xphe  38075  0he  38076  he0  38078  snhesn  38080  idhe  38081  frege54cor1c  38209  clsk1independent  38344  neicvgnvor  38414  amgm2d  38501  amgm3d  38502  amgm4d  38503  lhe4.4ex1a  38528  rusbcALT  38640  ipo0  38653  ifr0  38654  vk15.4j  38734  2sb5nd  38776  dfvd1ir  38789  dfvd2anir  38800  dfvd2ir  38802  dfvd3ir  38809  dfvd3anir  38812  iden2  38839  e0bir  39004  uun2221p1  39041  uun2221p2  39042  2sb5ndVD  39146  2sb5ndALT  39168  iunconnlem2  39171  fnchoice  39188  unisn0  39222  eliincex  39293  icof  39411  mptssid  39450  supminfxr  39694  fsumiunss  39807  climlimsupcex  40001  liminfltlimsupex  40013  liminflelimsupcex  40029  xlimrel  40046  resincncf  40088  dvnprodlem3  40163  mbf0  40173  volioc  40188  volico  40200  dmvolss  40202  volioof  40204  stoweidlem13  40230  stoweidlem34  40251  stirlinglem5  40295  stirlinglem13  40303  stirlingr  40307  fourierdlem42  40366  fourierdlem62  40385  fouriersw  40448  etransc  40500  salexct  40552  salexct2  40557  salgencntex  40561  sge0rnn0  40585  gsumge0cl  40588  sge00  40593  sge0resplit  40623  sge0reuz  40664  omeiunle  40731  0ome  40743  icoresmbl  40757  ovn0lem  40779  ovnhoilem1  40815  hspmbl  40843  ovolval5lem3  40868  nsssmfmbf  40987  mbfpsssmf  40991  smfresal  40995  smfmullem4  41001  smfpimbor1lem1  41005  smfpimbor1lem2  41006  aistia  41064  aisfina  41065  aiffnbandciffatnotciffb  41071  axorbciffatcxorb  41072  abnotbtaxb  41082  abnotataxb  41083  pfx2  41412  m3prm  41506  m7prm  41516  0noddALTV  41600  2noddALTV  41604  sbgoldbo  41675  nnsum3primes4  41676  evengpop3  41686  spr0nelg  41726  oddinmgm  41815  2zrngamgm  41939  2zrngaabl  41944  2zrngmmgm  41946  2zrngnring  41952  fldhmsubc  42084  fldhmsubcALTV  42102  eliunxp2  42112  zlmodzxzldeplem  42287  zlmodzxzldep  42293  ldepslinc  42298  ex-gte  42470  empty-surprise  42528  eximp-surprise2  42531  amgmw2d  42550