Theorem mpbir 209

Description: An inference from a biconditional, related to modus ponens. (Contributed by NM, 5-Aug-1993.)

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  904  mpbir3an  1163  xorexmid  1359  tru  1366  nic-mpALT  1482  nic-ax  1483  nic-axALT  1484  mpgbir  1598  nfxfr  1618  19.35ri  1656  ax6ev  1709  exan  1899  cbvex2OLD  1976  ax13  1994  sbtOLD  2077  moanmo  2332  moaneuOLD  2334  axi12  2412  axext2  2415  eqeltri  2503  nfcxfr  2566  neir  2601  neirr  2603  exmidne  2604  eqnetri  2615  nesymir  2639  nelir  2698  mprgbir  2776  vex  2965  issetri  2969  moeq  3124  cdeqi  3160  eqsstri  3374  3sstr4i  3383  rabrsn  3933  tpid1  3976  tpid2  3977  tpid3  3979  pwv  4078  uni0  4106  eqbrtri  4299  tr0  4384  trv  4385  zfrep4  4399  zfnuleu  4406  axnulALT  4407  0ex  4410  inex1  4421  0elpw  4449  axpow2  4460  axpow3  4461  pwex  4463  dvdemo1  4515  zfpair2  4520  exss  4543  moop2  4574  pwundif  4615  po0  4643  epse  4690  0elon  4759  relsnop  4931  relxp  4934  rel0  4951  relopabi  4952  eliunxp  4964  opeliunxp2  4965  dmi  5041  xpidtr  5208  xpima  5268  cnvcnv  5278  dmsn0  5294  cnvsn0  5295  funmpt  5442  funmpt2  5443  isarep2  5486  fresaunres2  5571  f0  5580  f10  5660  f1o00  5661  f1oi  5664  f1osn  5666  brprcneu  5672  opabiotafun  5740  fvopab3ig  5759  opabex  5933  eufnfv  5938  canth  6036  ncanth  6037  mpt2fun  6181  reldmmpt2  6190  ovid  6196  ovidig  6197  ovidi  6198  ovig  6201  ov3  6216  caovmo  6289  relmptopab  6297  porpss  6353  uniex2  6364  snnex  6371  tfinds2  6463  finds  6491  finds2  6493  oprabex  6554  oprabex3  6555  f1stres  6587  f2ndres  6588  relmpt2opab  6644  tpos0  6764  issmo  6795  tfrlem6  6827  tfrlem8  6829  tfrlem16  6838  tfr1a  6839  tfr1  6842  tz7.44lem1  6847  seqomlem2  6892  seqomlem3  6893  seqomlem4  6894  fnseqom  6896  abianfp  6900  0lt1o  6932  0we1  6934  eqer  7122  ecopover  7192  th3qcor  7196  mapsnf1o3  7249  ssdomg  7343  ensn1  7361  snfi  7378  xpcomf1o  7388  map2xp  7469  limensuci  7475  sdom1  7500  unblem4  7555  fidomdm  7581  marypha1lem  7671  hartogslem1  7744  hartogs  7746  card2on  7757  ruALT  7805  inf2  7817  inf3lem6  7827  infeq5i  7830  zfinf2  7836  cantnflt  7868  cantnfltOLD  7898  cantnfOLD  7911  mapfienOLD  7915  cnfcom  7921  cnfcomOLD  7929  trcl  7936  tz9.1c  7938  tc2  7950  r1funlim  7961  r1fnon  7962  karden  8090  tskwe  8108  cardprclem  8137  pm54.43  8158  r0weon  8167  iunmapdisj  8181  alephfnon  8223  alephfplem4  8265  alephfp  8266  alephval3  8268  aceq3lem  8278  kmlem2  8308  cda1dif  8333  ackbij1  8395  ackbij2lem2  8397  ackbij2  8400  infpssrlem3  8462  hsmexlem4  8586  hsmexlem5  8587  axdc3lem4  8610  ac2  8618  axac3  8621  ac6  8637  axdclem2  8677  ondomon  8715  alephsucpw  8722  pwcfsdom  8735  cfpwsdom  8736  smobeth  8738  axpowndlem3  8752  axpowndlem3OLD  8753  zfcndun  8770  zfcndpow  8771  zfcndinf  8773  zfcndac  8774  wunex2  8893  uniwun  8895  wuncval2  8902  grur1  8975  axgroth5  8979  axgroth2  8980  axgroth6  8983  axgroth3  8986  grothtsk  8990  inaprc  8991  ltsopi  9045  dmaddpi  9047  dmmulpi  9048  1lt2pi  9062  nqerf  9087  addnqf  9105  mulnqf  9106  1lt2nq  9130  m1p1sr  9247  m1m1sr  9248  0lt1sr  9250  axaddf  9300  axmulf  9301  ax1cn  9304  subaddrii  9685  ixi  9953  recgt0ii  10226  nn1suc  10331  neg1lt0  10416  4d2e2  10466  arch  10564  un0mulcl  10602  nummac  10775  uzf  10852  indstr  10911  mnfltpnf  11094  ixxf  11298  ioof  11375  fzf  11428  fzp1disj  11500  fzof  11534  om2uzrani  11759  om2uzf1oi  11760  uzrdglem  11764  uzrdgfni  11765  uzrdg0i  11766  ltwenn  11769  hashgf1o  11777  axdc4uzlem  11788  sq0  11941  irec  11949  hashkf  12089  hashf  12094  hash0  12119  hashsslei  12160  hashxplem  12179  hashbclem  12189  hashf1lem1  12192  wrdexg  12228  wrd0  12236  revs1  12389  0csh0  12414  cshw1  12440  cats1fvn  12469  climmo  13019  fsumcom2  13225  ackbijnn  13274  incexclem  13282  infcvgaux1i  13302  efcvgfsum  13354  cos1bnd  13454  cos2bnd  13455  znnen  13478  qnnen  13479  aleph1re  13510  dvdslelem  13560  3dvds  13579  divalglem5  13584  bitsf  13606  sadcaddlem  13636  sadadd2lem  13638  sadadd3  13640  sadaddlem  13645  isprm3  13755  2prm  13762  phicl2  13826  pockthi  13951  unbenlem  13952  prmrec  13966  vdwlem13  14037  vdwnn  14042  ramcl2  14060  mod2xnegi  14083  modsubi  14084  structcnvcnv  14168  structfun  14169  setsres  14185  strfv  14191  strlemor1  14248  strleun  14251  0rest  14351  firest  14354  restid  14355  prdsval  14376  prdsbas  14378  prdsplusg  14379  prdsmulr  14380  prdsvsca  14381  prdsds  14385  imasaddfnlem  14449  imasvscafn  14458  oppchomfval  14636  oppcbas  14640  2oppchomf  14646  rescbas  14725  rescco  14728  rescabs  14729  idfucl  14774  wunnat  14849  homarel  14887  dmaf  14900  cdaf  14901  catcfuccl  14960  relxpchom  14974  catcxpccl  15000  oppchofcl  15053  oyoncl  15063  odubas  15286  letsr  15380  mgmidmo  15401  releqg  15708  ga0  15796  oppglem  15845  psgnunilem3  15982  psgnunilem4  15983  efgval  16194  efger  16195  efgsp1  16214  efgsfo  16216  efgredleme  16220  efgredlem  16224  efgred  16225  cygctb  16348  gsum2d2lem  16439  gsum2d2  16440  gsumcom2  16441  dprd2d2  16517  pgpfaclem1  16556  mgplem  16570  mgpress  16576  opprlem  16654  reldvdsr  16670  00lsp  16984  sralem  17180  srasca  17184  sravsca  17185  psrvscafval  17395  opsrbaslem  17491  psrbag0  17508  00ply1bas  17593  ply1plusgfvi  17595  zlmsca  17794  znbaslem  17813  resubdrg  17880  ocvfval  17933  ocv0  17944  cssval  17949  thlbas  17963  thlle  17964  islinds2  18084  matsca  18158  m2detleib  18279  eltopspOLD  18365  tgdom  18425  tgidm  18427  indistps2ALT  18460  restbas  18604  resttopon  18607  rest0  18615  leordtval2  18658  iocpnfordt  18661  icomnfordt  18662  iooordt  18663  cnpfval  18680  iscnp2  18685  ist1-3  18795  1stcfb  18891  islly2  18930  1stckgen  18969  ptbasfi  18996  xkotf  19000  dfac14  19033  opnfbas  19257  hauspwpwf1  19402  alexsubALTlem4  19464  alexsubALT  19465  ptcmplem5  19470  cnextrel  19477  ust0  19636  tuslem  19684  0met  19783  prdsdsf  19784  prdsxmetlem  19785  prdsmet  19787  setsmsbas  19892  setsmsds  19893  prdsbl  19908  tngds  20076  qtopbaslem  20179  xrtgioo  20225  xrsdsre  20229  zcld  20232  recld2  20233  sszcld  20236  reperflem  20237  retopcon  20248  iccpnfcnv  20358  bndth  20372  ishtpy  20386  nmoleub2lem2  20513  recmet  20676  resscdrg  20712  ishl2  20724  recms  20726  ehlbase  20752  volf  20854  iundisj2  20872  volsup  20879  icombl  20887  ioombl  20888  ismbf3d  20974  0plef  20992  0pledm  20993  itg1ge0  21006  mbfi1fseqlem5  21039  itg2addlem  21078  iblcnlem1  21107  reldv  21187  limciun  21211  dvexp  21269  dveflem  21293  lhop1lem  21327  lhop  21330  elply2  21549  elplyd  21555  ply1term  21557  ply0  21561  plymullem  21569  qaa  21674  pserulm  21772  pserdvlem2  21778  efcn  21793  sincosq1lem  21844  tangtx  21852  sincos4thpi  21860  sincos6thpi  21862  pige3  21864  efif1olem4  21886  logf1o  21901  relogf1o  21903  log1  21919  loge  21920  relogiso  21931  dvrelog  21967  relogcn  21968  logcn  21977  cxpcn3  22071  resqrcn  22072  leibpi  22222  log2ublem1  22226  birthday  22233  emcllem5  22278  harmonicbnd  22282  harmonicbnd2  22283  emgt0  22285  harmonicbnd3  22286  ppiltx  22400  ppiublem1  22426  ppiub  22428  bclbnd  22504  bpos1lem  22506  bposlem8  22515  lgsquadlem2  22579  2sqlem9  22597  2sqlem10  22598  chebbnd1  22606  selberg2lem  22684  pntrsumo1  22699  selbergsb  22709  pntpbnd  22722  ttgval  22944  ttglem  22945  cchhllem  22956  ax5seglem7  23004  axlowdimlem4  23014  axlowdimlem6  23016  axlowdimlem7  23017  axlowdimlem10  23020  axlowdimlem13  23023  axlowdimlem16  23026  axlowdimlem17  23027  axlowdim  23030  uhgra0  23066  umgra0  23082  usgra0  23112  usgra1v  23131  cusgraexilem2  23198  cusgrasizeindslem2  23205  0wlk  23267  0trl  23268  wlkntrllem2  23282  wlkntrl  23284  0pth  23292  1pthonlem1  23311  usgrcyclnl2  23350  4cycl4dv  23376  vdgrf  23391  umgrabi  23427  vdegp1ai  23428  vdegp1bi  23429  konigsberg  23431  ex-dif  23453  ex-in  23455  ex-eprel  23463  ex-id  23464  ex-fl  23477  avril1  23479  2bornot2b  23480  grposn  23525  issubgoi  23620  0vfval  23807  vsfval  23836  ajmoi  24082  ajfuni  24083  normlem2  24336  norm3adifii  24373  hhip  24402  hlim0  24461  hlimcaui  24462  hlimf  24463  hhssnv  24488  shscli  24543  shsval2i  24613  h1de2i  24779  fh3i  24849  fh4i  24850  cm2mi  24852  qlaxr3i  24862  mayetes3i  24956  ho0f  24978  hoif  24981  hodidi  25014  ho0subi  25022  hosd1i  25049  adjmo  25059  nmopsetn0  25092  nmfnsetn0  25105  funadj  25113  funcnvadj  25120  nmcexi  25253  cnlnadjlem8  25301  nmoptri2i  25326  opsqrlem4  25370  hmopidmchi  25378  pjoci  25407  pjinvari  25418  abrexdomjm  25712  elim2ifim  25731  iundisj2f  25756  rinvf1o  25773  funcnvmptOLD  25810  dfcnv2  25818  snct  25835  dmct  25838  fpwrelmap  25858  iundisj2fi  25904  nn0srg  26063  rge0srg  26064  gsumle  26098  reofld  26162  rearchi  26164  xrge0slmod  26166  xrge0iifcnv  26217  xrge0pluscn  26224  zlmds  26247  zlmtset  26248  cnzh  26253  rezh  26254  qqhre  26300  esumfsup  26373  esumpcvgval  26381  hasheuni  26388  esumcvg  26389  dmsigagen  26441  measvuni  26482  voliune  26499  volfiniune  26500  ddemeas  26506  br2base  26538  dya2iocuni  26552  eulerpartlem1  26598  eulerpartlemt  26602  eulerpartgbij  26603  fib0  26630  fib6  26637  coinfliprv  26713  ballotlem2  26719  ballotlemfc0  26723  ballotlemfcc  26724  ballotlemic  26737  ballotlem7  26766  ballotth  26768  plymul02  26795  signswmnd  26806  lgamgulm2  26870  lgamcvglem  26874  gamf  26877  subfacp1lem5  26920  subfacp1lem6  26921  kur14lem9  26950  cvmcov2  27012  cvmliftlem1  27022  cvmliftlem4  27025  cvmliftlem5  27026  problem5  27150  ghomgrpilem2  27152  relexp0  27178  relexpsucr  27179  relexpsucl  27181  dfrtrclrec2  27192  rtrclreclem.refl  27193  rtrclreclem.subset  27194  rtrclreclem.min  27196  dfrtrcl2  27197  brtpid1  27224  brtpid2  27225  brtpid3  27226  fzp1nel  27244  fprodcom2  27342  faclimlem1  27396  domep  27453  axextndbi  27465  poseq  27561  wfrlem6  27576  wfrlem14  27584  wfrlem16  27586  frrlem10  27626  sltval2  27644  nosgnn0i  27647  brv  27755  txprel  27757  relsset  27766  relbigcup  27775  fvbigcup  27780  fnsingle  27797  fvsingle  27798  snelsingles  27800  funimage  27806  fullfunfnv  27824  imagesset  27831  funtransport  27909  colinrel  27935  funray  28018  funline  28020  bpolylem  28038  bpoly3  28048  bpoly4  28049  0hf  28062  waj-ax  28108  lukshef-ax2  28109  arg-ax  28110  limsucncmpi  28139  mblfinlem1  28272  mblfinlem2  28273  ismblfin  28276  voliunnfl  28279  cnambfre  28284  dvtanlem  28285  comppfsc  28423  neibastop2lem  28425  filnetlem3  28445  cover2  28451  abrexdom  28468  fdc  28485  cncfres  28508  heibor1lem  28552  bicontr  28724  an12i  28745  tsim1  28785  moxfr  28873  mapfzcons1  28898  diophrw  28942  0dioph  28962  vdioph  28963  rabren3dioph  28999  2nn0ind  29131  rpnnen3  29226  kelac2lem  29262  frlmpwfi  29298  areaquad  29437  lhe4.4ex1a  29448  rusbcALT  29538  ipo0  29550  ifr0  29551  fnchoice  29596  stoweidlem13  29654  stoweidlem34  29675  stirlinglem5  29719  stirlinglem13  29727  stirlingr  29731  aistia  29757  aisfina  29758  aiffnbandciffatnotciffb  29764  axorbciffatcxorb  29765  abnotbtaxb  29776  abnotataxb  29777  usgra2pthspth  30141  usgra2pthlem1  30146  wwlknext  30202  wwlknfi  30216  disjxwwlkn  30410  frgra0  30432  numclwwlkdisj  30519  numclwwlk3lem  30547  eliunxp2  30566  pmtrsn  30601  zlmodzxzldeplem  30749  zlmodzxzldep  30755  ldepslinc  30760  ex-gte  30773  AnelBC  30808  empty-surprise  30841  eximp-surprise2  30844  vk15.4j  30934  2sb5nd  30970  dfvd1ir  30987  dfvd2anir  30999  dfvd2ir  31001  dfvd3ir  31008  dfvd3anir  31011  iden2  31038  e0bir  31212  uun2221p1  31249  uun2221p2  31250  2sb5ndVD  31348  2sb5ndALT  31370  iunconlem2  31373  bnj226  31427  bnj1101  31480  bnj110  31553  bnj149  31570  bnj150  31571  bnj151  31572  bnj517  31580  bnj580  31608  bnj865  31618  bnj900  31624  bnj996  31650  bnj1110  31675  bnj1133  31682  bnj1128  31683  bnj1145  31686  bnj1137  31688  bnj1171  31693  bnj1176  31698  bj-babylob  31786  bj-nfv  31824  bj-spimfw  31826  bj-dvdemo1  31943  bj-vexwv  31976  bj-disjcsn  32023  bj-snsetex  32039  bj-0eltag  32054  bj-2upln0  32099  bj-2upln1upl  32100  elimhyps  32185  dedths  32186  renegclALT  32187  hlhilslem  35159