Theorem mpbir 209

Description: An inference from a biconditional, related to modus ponens. (Contributed by NM, 28-Dec-1992.)

Hypotheses

Ref	Expression
mpbir.min	|- ps
mpbir.maj	|- ( ph <-> ps )

Assertion

Ref	Expression
mpbir	|- ph

Proof of Theorem mpbir

Step	Hyp	Ref	Expression
1		mpbir.min	. 2 |- ps
2		mpbir.maj	. . 3 |- ( ph <-> ps )
3	2	biimpri 206	. 2 |- ( ps -> ph )
4	1, 3	ax-mp 5	1 |- ph

Syntax hints:   <-> wb 184

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 185

This theorem is referenced by:  pm5.74ri  246  con4bii  297  orri  376  imorri  414  imnani  423  mpbir2an  918  mpbir3an  1178  xorexmid  1376  tru  1383  nic-mpALT  1489  nic-ax  1490  nic-axALT  1491  mpgbir  1605  nfxfr  1625  19.35ri  1667  ax6ev  1721  exan  1922  cbvex2OLD  2002  ax13  2020  euequ1  2281  moanmo  2357  moaneuOLD  2359  axi12  2443  axext2  2446  eqeltri  2551  nfcxfr  2627  neir  2667  neirr  2671  exmidneOLD  2673  nesymirOLD  2743  eqnetri  2763  nelir  2803  mprgbir  2828  vex  3116  issetri  3120  moeq  3279  cdeqi  3316  eqsstri  3534  3sstr4i  3543  rabrsn  4097  tpid1  4140  tpid2  4141  tpid3  4143  pwv  4244  uni0  4272  eqbrtri  4466  tr0  4551  trv  4552  zfrep4  4566  zfnuleu  4573  axnulALT  4574  0ex  4577  inex1  4588  0elpw  4616  axpow2  4627  axpow3  4628  pwex  4630  dvdemo1  4682  zfpair2  4687  exss  4710  moop2  4742  pwundif  4787  po0  4815  epse  4862  0elon  4931  relsnop  5105  relxp  5108  rel0  5125  relopabi  5126  eliunxp  5138  opeliunxp2  5139  dmi  5215  xpidtr  5387  xpima  5447  cnvcnv  5457  dmsn0  5473  cnvsn0  5474  funmpt  5622  funmpt2  5623  isarep2  5666  fresaunres2  5755  f0  5764  f10  5845  f1o00  5846  f1oi  5849  f1osn  5851  brprcneu  5857  opabiotafun  5926  fvopab3ig  5945  opabex  6127  eufnfv  6132  canth  6240  ncanth  6241  mpt2fun  6386  reldmmpt2  6395  ovid  6401  ovidig  6402  ovidi  6403  ovig  6406  ov3  6421  caovmo  6494  relmptopab  6505  porpss  6566  uniex2  6577  snnex  6584  tfinds2  6676  finds  6704  finds2  6706  oprabex  6769  oprabex3  6770  f1stres  6803  f2ndres  6804  relmpt2opab  6862  tpos0  6982  issmo  7016  tfrlem6  7048  tfrlem8  7050  tfrlem16  7059  tfr1a  7060  tfr1  7063  tz7.44lem1  7068  seqomlem2  7113  seqomlem3  7114  seqomlem4  7115  fnseqom  7117  0lt1o  7151  0we1  7153  eqer  7341  ecopover  7412  mapsnf1o3  7464  ssdomg  7558  ensn1  7576  snfi  7593  xpcomf1o  7603  map2xp  7684  limensuci  7690  sdom1  7716  unblem4  7771  fidomdm  7798  marypha1lem  7889  hartogslem1  7963  hartogs  7965  card2on  7976  ruALT  8024  inf2  8036  inf3lem6  8046  infeq5i  8049  zfinf2  8055  cantnflt  8087  cantnfltOLD  8117  cantnfOLD  8130  mapfienOLD  8134  cnfcom  8140  cnfcomOLD  8148  trcl  8155  tz9.1c  8157  tc2  8169  r1funlim  8180  r1fnon  8181  karden  8309  tskwe  8327  cardprclem  8356  pm54.43  8377  r0weon  8386  iunmapdisj  8400  alephfnon  8442  alephfplem4  8484  alephfp  8485  alephval3  8487  aceq3lem  8497  kmlem2  8527  cda1dif  8552  ackbij1  8614  ackbij2lem2  8616  ackbij2  8619  infpssrlem3  8681  hsmexlem4  8805  hsmexlem5  8806  axdc3lem4  8829  ac2  8837  axac3  8840  ac6  8856  axdclem2  8896  ondomon  8934  alephsucpw  8941  pwcfsdom  8954  cfpwsdom  8955  smobeth  8957  axpowndlem3  8971  axpowndlem3OLD  8972  zfcndun  8989  zfcndpow  8990  zfcndinf  8992  zfcndac  8993  wunex2  9112  uniwun  9114  wuncval2  9121  grur1  9194  axgroth5  9198  axgroth2  9199  axgroth6  9202  axgroth3  9205  grothtsk  9209  inaprc  9210  ltsopi  9262  dmaddpi  9264  dmmulpi  9265  1lt2pi  9279  nqerf  9304  addnqf  9322  mulnqf  9323  1lt2nq  9347  m1p1sr  9465  m1m1sr  9466  0lt1sr  9468  axaddf  9518  axmulf  9519  ax1cn  9522  subaddrii  9904  ixi  10174  recgt0ii  10447  nn1suc  10553  neg1lt0  10638  4d2e2  10688  arch  10788  un0mulcl  10826  nummac  11004  uzf  11081  indstr  11146  mnfltpnf  11331  ixxf  11535  ioof  11618  fzf  11672  fzp1disj  11734  fzof  11790  om2uzrani  12027  om2uzf1oi  12028  uzrdglem  12032  uzrdgfni  12033  uzrdg0i  12034  ltwenn  12037  hashgf1o  12045  axdc4uzlem  12056  sq0  12223  irec  12231  hashkf  12371  hashf  12376  hash0  12401  hashsslei  12445  hashxplem  12453  hashbclem  12463  hashf1lem1  12466  wrdexg  12519  wrd0  12527  revs1  12698  0csh0  12723  cshw1  12749  cats1fvn  12782  climmo  13339  fsumcom2  13548  ackbijnn  13599  incexclem  13607  infcvgaux1i  13627  efcvgfsum  13679  cos1bnd  13779  cos2bnd  13780  znnen  13803  qnnen  13804  aleph1re  13835  dvdslelem  13885  3dvds  13905  divalglem5  13910  bitsf  13932  sadcaddlem  13962  sadadd2lem  13964  sadadd3  13966  sadaddlem  13971  isprm3  14081  2prm  14088  phicl2  14153  pockthi  14280  unbenlem  14281  prmrec  14295  vdwlem13  14366  vdwnn  14371  ramcl2  14389  mod2xnegi  14412  modsubi  14413  structcnvcnv  14497  structfun  14498  setsres  14514  strfv  14520  strlemor1  14578  strleun  14581  0rest  14681  firest  14684  restid  14685  prdsval  14706  prdsbas  14708  prdsplusg  14709  prdsmulr  14710  prdsvsca  14711  prdsds  14715  imasaddfnlem  14779  imasvscafn  14788  oppchomfval  14966  oppcbas  14970  2oppchomf  14976  rescbas  15055  rescco  15058  rescabs  15059  idfucl  15104  wunnat  15179  homarel  15217  dmaf  15230  cdaf  15231  catcfuccl  15290  relxpchom  15304  catcxpccl  15330  oppchofcl  15383  oyoncl  15393  odubas  15616  letsr  15710  mgmidmo  15731  releqg  16043  ga0  16131  oppglem  16180  psgnunilem3  16317  psgnunilem4  16318  pmtrsn  16340  efgval  16531  efger  16532  efgsp1  16551  efgsfo  16553  efgredleme  16557  efgredlem  16561  efgred  16562  cygctb  16685  gsum2d2lem  16792  gsum2d2  16793  gsumcom2  16794  dprd2d2  16883  pgpfaclem1  16922  mgplem  16936  mgpress  16942  opprlem  17061  reldvdsr  17077  00lsp  17410  sralem  17606  srasca  17610  sravsca  17611  psrvscafval  17814  opsrbaslem  17913  psrbag0  17930  00ply1bas  18052  ply1plusgfvi  18054  nn0srg  18254  rge0srg  18255  zlmsca  18325  znbaslem  18344  resubdrg  18411  ocvfval  18464  ocv0  18475  cssval  18480  thlbas  18494  thlle  18495  islinds2  18615  matsca  18684  m2detleib  18900  eltopspOLD  19186  tgdom  19246  tgidm  19248  indistps2ALT  19281  restbas  19425  resttopon  19428  rest0  19436  leordtval2  19479  iocpnfordt  19482  icomnfordt  19483  iooordt  19484  cnpfval  19501  iscnp2  19506  ist1-3  19616  1stcfb  19712  islly2  19751  1stckgen  19790  ptbasfi  19817  xkotf  19821  dfac14  19854  opnfbas  20078  hauspwpwf1  20223  alexsubALTlem4  20285  alexsubALT  20286  ptcmplem5  20291  cnextrel  20298  ust0  20457  tuslem  20505  0met  20604  prdsdsf  20605  prdsxmetlem  20606  prdsmet  20608  setsmsbas  20713  setsmsds  20714  prdsbl  20729  tngds  20897  qtopbaslem  21000  xrtgioo  21046  xrsdsre  21050  zcld  21053  recld2  21054  sszcld  21057  reperflem  21058  retopcon  21069  iccpnfcnv  21179  bndth  21193  ishtpy  21207  nmoleub2lem2  21334  recmet  21497  resscdrg  21533  ishl2  21545  recms  21547  ehlbase  21573  volf  21675  iundisj2  21694  volsup  21701  icombl  21709  ioombl  21710  ismbf3d  21796  0plef  21814  0pledm  21815  itg1ge0  21828  mbfi1fseqlem5  21861  itg2addlem  21900  iblcnlem1  21929  reldv  22009  limciun  22033  dvexp  22091  dveflem  22115  lhop1lem  22149  lhop  22152  elply2  22328  elplyd  22334  ply1term  22336  ply0  22340  plymullem  22348  qaa  22453  pserulm  22551  pserdvlem2  22557  efcn  22572  sincosq1lem  22623  tangtx  22631  sincos4thpi  22639  sincos6thpi  22641  pige3  22643  efif1olem4  22665  logf1o  22680  relogf1o  22682  log1  22698  loge  22699  relogiso  22710  dvrelog  22746  relogcn  22747  logcn  22756  cxpcn3  22850  resqrtcn  22851  leibpi  23001  log2ublem1  23005  birthday  23012  emcllem5  23057  harmonicbnd  23061  harmonicbnd2  23062  emgt0  23064  harmonicbnd3  23065  ppiltx  23179  ppiublem1  23205  ppiub  23207  bclbnd  23283  bpos1lem  23285  bposlem8  23294  lgsquadlem2  23358  2sqlem9  23376  2sqlem10  23377  chebbnd1  23385  selberg2lem  23463  pntrsumo1  23478  selbergsb  23488  pntpbnd  23501  istrkg2ld  23586  isismt  23649  ttgval  23854  ttglem  23855  cchhllem  23866  ax5seglem7  23914  axlowdimlem4  23924  axlowdimlem6  23926  axlowdimlem7  23927  axlowdimlem10  23930  axlowdimlem13  23933  axlowdimlem16  23936  axlowdimlem17  23937  axlowdim  23940  uhgra0  23985  umgra0  24001  usgra0  24046  usgra1v  24066  cusgraexilem2  24143  cusgrasizeindslem2  24150  0wlk  24223  0trl  24224  wlkntrllem2  24238  wlkntrl  24240  0pth  24248  1pthonlem1  24267  usgrcyclnl2  24317  4cycl4dv  24343  wwlknext  24400  wwlknfi  24414  disjxwwlkn  24421  vdgrf  24574  umgrabi  24659  vdegp1ai  24660  vdegp1bi  24661  konigsberg  24663  frgra0  24670  numclwwlkdisj  24757  numclwwlk3lem  24785  ex-dif  24821  ex-in  24823  ex-eprel  24831  ex-id  24832  ex-fl  24845  avril1  24847  2bornot2b  24848  grposn  24893  issubgoi  24988  0vfval  25175  vsfval  25204  ajmoi  25450  ajfuni  25451  normlem2  25704  norm3adifii  25741  hhip  25770  hlim0  25829  hlimcaui  25830  hlimf  25831  hhssnv  25856  shscli  25911  shsval2i  25981  h1de2i  26147  fh3i  26217  fh4i  26218  cm2mi  26220  qlaxr3i  26230  mayetes3i  26324  ho0f  26346  hoif  26349  hodidi  26382  ho0subi  26390  hosd1i  26417  adjmo  26427  nmopsetn0  26460  nmfnsetn0  26473  funadj  26481  funcnvadj  26488  nmcexi  26621  cnlnadjlem8  26669  nmoptri2i  26694  opsqrlem4  26738  hmopidmchi  26746  pjoci  26775  pjinvari  26786  abrexdomjm  27079  elim2ifim  27097  iundisj2f  27122  rinvf1o  27145  funcnvmptOLD  27181  dfcnv2  27189  snct  27206  dmct  27209  fpwrelmap  27228  iundisj2fi  27270  gsumle  27433  reofld  27493  rearchi  27495  xrge0slmod  27497  xrge0iifcnv  27551  xrge0pluscn  27558  zlmds  27581  zlmtset  27582  cnzh  27587  rezh  27588  qqhre  27634  esumfsup  27716  esumpcvgval  27724  hasheuni  27731  esumcvg  27732  dmsigagen  27784  measvuni  27825  voliune  27841  volfiniune  27842  ddemeas  27848  br2base  27880  dya2iocuni  27894  oms0  27906  eulerpartlem1  27946  eulerpartlemt  27950  eulerpartgbij  27951  fib0  27978  fib6  27985  coinfliprv  28061  ballotlem2  28067  ballotlemfc0  28071  ballotlemfcc  28072  ballotlemic  28085  ballotlem7  28114  ballotth  28116  plymul02  28143  signswmnd  28154  lgamgulm2  28218  lgamcvglem  28222  gamf  28225  subfacp1lem5  28268  subfacp1lem6  28269  kur14lem9  28298  cvmcov2  28360  cvmliftlem1  28370  cvmliftlem4  28373  cvmliftlem5  28374  problem5  28498  ghomgrpilem2  28501  relexp0  28527  relexpsucr  28528  relexpsucl  28530  dfrtrclrec2  28541  rtrclreclem.refl  28542  rtrclreclem.subset  28543  rtrclreclem.min  28545  dfrtrcl2  28546  brtpid1  28573  brtpid2  28574  brtpid3  28575  fzp1nel  28593  fprodcom2  28691  faclimlem1  28745  domep  28802  axextndbi  28814  poseq  28910  wfrlem6  28925  wfrlem14  28933  wfrlem16  28935  frrlem10  28975  sltval2  28993  nosgnn0i  28996  brv  29104  txprel  29106  relsset  29115  relbigcup  29124  fvbigcup  29129  fnsingle  29146  fvsingle  29147  snelsingles  29149  funimage  29155  fullfunfnv  29173  imagesset  29180  funtransport  29258  colinrel  29284  funray  29367  funline  29369  bpolylem  29387  bpoly3  29397  bpoly4  29398  0hf  29411  waj-ax  29456  lukshef-ax2  29457  arg-ax  29458  limsucncmpi  29487  mblfinlem1  29628  mblfinlem2  29629  ismblfin  29632  voliunnfl  29635  cnambfre  29640  dvtanlem  29641  comppfsc  29779  neibastop2lem  29781  filnetlem3  29801  cover2  29807  abrexdom  29824  fdc  29841  cncfres  29864  heibor1lem  29908  bicontr  30080  an12i  30101  tsim1  30141  ac6s6f  30185  moxfr  30228  mapfzcons1  30253  diophrw  30296  0dioph  30316  vdioph  30317  rabren3dioph  30353  2nn0ind  30485  rpnnen3  30578  kelac2lem  30614  frlmpwfi  30650  3lcm2e6  30819  lhe4.4ex1a  30834  rusbcALT  30924  ipo0  30936  ifr0  30937  fnchoice  30982  halffl  31070  iooinlbub  31098  resincncf  31213  0cnf  31215  mbf0  31275  iblempty  31283  iblsplit  31284  volioc  31290  stoweidlem13  31313  stoweidlem34  31334  stirlinglem5  31378  stirlinglem13  31386  stirlingr  31390  dirkercncflem2  31404  fourierdlem42  31449  fourierdlem43  31450  fourierdlem57  31464  fourierdlem62  31469  fourierdlem103  31510  fourierdlem104  31511  sqwvfoura  31529  sqwvfourb  31530  fouriersw  31532  aistia  31559  aisfina  31560  aiffnbandciffatnotciffb  31566  axorbciffatcxorb  31567  abnotbtaxb  31578  abnotataxb  31579  usgra2pthspth  31820  usgra2pthlem1  31822  uhg0e  31845  eliunxp2  31987  zlmodzxzldeplem  32180  zlmodzxzldep  32186  ldepslinc  32191  ex-gte  32204  AnelBC  32239  empty-surprise  32278  eximp-surprise2  32281  vk15.4j  32377  2sb5nd  32413  dfvd1ir  32430  dfvd2anir  32441  dfvd2ir  32443  dfvd3ir  32450  dfvd3anir  32453  iden2  32480  e0bir  32654  uun2221p1  32691  uun2221p2  32692  2sb5ndVD  32790  2sb5ndALT  32812  iunconlem2  32815  bnj226  32869  bnj1101  32922  bnj110  32995  bnj149  33012  bnj150  33013  bnj151  33014  bnj517  33022  bnj580  33050  bnj865  33060  bnj900  33066  bnj996  33092  bnj1110  33117  bnj1133  33124  bnj1128  33125  bnj1145  33128  bnj1137  33130  bnj1171  33135  bnj1176  33140  bj-babylob  33274  bj-nfv  33309  bj-nalnalimiOLD  33312  bj-dvdemo1  33469  bj-disjcsn  33586  bj-snsetex  33602  bj-0eltag  33617  bj-2upln0  33662  bj-2upln1upl  33663  elimhyps  33764  dedths  33765  renegclALT  33766  hlhilslem  36738