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  295  orri  374  imorri  412  imnani  421  mpbir2an  918  mpbir3an  1176  xorexmid  1381  tru  1403  nic-mpALT  1512  nic-ax  1513  nic-axALT  1514  mpgbir  1630  nfxfr  1653  19.35ri  1698  ax5e  1714  ax6ev  1757  exan  1981  ax13  2053  euequ1  2224  moanmo  2284  axi12  2358  axext2  2361  eqeltri  2466  nfcxfr  2542  neir  2582  neirr  2586  exmidneOLD  2588  nesymirOLD  2658  eqnetri  2678  nelir  2718  mprgbir  2746  vex  3037  issetri  3041  moeq  3200  cdeqi  3237  eqsstri  3447  3sstr4i  3456  rabrsn  4014  tpid1  4057  tpid2  4058  tpid3  4060  pwv  4162  uni0  4190  eqbrtri  4386  tr0  4471  trv  4472  zfrep4  4486  zfnuleu  4493  axnulALT  4494  0ex  4497  inex1  4506  0elpw  4534  axpow2  4545  axpow3  4546  pwex  4548  dvdemo1  4597  zfpair2  4602  exss  4625  moop2  4656  pwundif  4701  po0  4729  epse  4776  0elon  4845  relsnop  5020  relxp  5023  rel0  5039  relopabi  5040  eliunxp  5053  opeliunxp2  5054  dmi  5130  xpidtr  5302  xpima  5359  cnvcnv  5368  dmsn0  5383  cnvsn0  5384  funmpt  5532  funmpt2  5533  isarep2  5576  fresaunres2  5665  f0  5674  f10  5755  f1o00  5756  f1oi  5759  f1osn  5761  brprcneu  5767  opabiotafun  5835  fvopab3ig  5854  opabex  6042  eufnfv  6047  canth  6155  ncanth  6156  mpt2fun  6303  reldmmpt2  6312  ovid  6318  ovidig  6319  ovidi  6320  ovig  6323  ov3  6338  caovmo  6411  relmptopab  6422  porpss  6483  uniex2  6494  snnex  6505  tfinds2  6597  finds  6625  finds2  6627  oprabex  6687  oprabex3  6688  f1stres  6721  f2ndres  6722  relmpt2opab  6781  tpos0  6903  issmo  6937  tfrlem6  6969  tfrlem8  6971  tfrlem16  6980  tfr1a  6981  tfr1  6984  tz7.44lem1  6989  seqomlem2  7034  seqomlem3  7035  seqomlem4  7036  fnseqom  7038  0lt1o  7072  0we1  7074  eqer  7262  ecopover  7333  mapsnf1o3  7386  ssdomg  7480  ensn1  7498  snfi  7515  xpcomf1o  7525  map2xp  7606  limensuci  7612  sdom1  7636  unblem4  7690  fidomdm  7717  marypha1lem  7808  hartogslem1  7882  hartogs  7884  card2on  7895  ruALT  7942  inf2  7954  inf3lem6  7964  infeq5i  7967  zfinf2  7973  cantnflt  8004  cantnfltOLD  8034  cantnfOLD  8047  mapfienOLD  8051  cnfcom  8057  cnfcomOLD  8065  trcl  8072  tz9.1c  8074  tc2  8086  r1funlim  8097  r1fnon  8098  karden  8226  tskwe  8244  cardprclem  8273  pm54.43  8294  r0weon  8303  iunmapdisj  8317  alephfnon  8359  alephfplem4  8401  alephfp  8402  alephval3  8404  aceq3lem  8414  kmlem2  8444  cda1dif  8469  ackbij1  8531  ackbij2lem2  8533  ackbij2  8536  infpssrlem3  8598  hsmexlem4  8722  hsmexlem5  8723  axdc3lem4  8746  ac2  8754  axac3  8757  ac6  8773  axdclem2  8813  ondomon  8851  alephsucpw  8858  pwcfsdom  8871  cfpwsdom  8872  smobeth  8874  axpowndlem3  8887  zfcndun  8904  zfcndpow  8905  zfcndinf  8907  zfcndac  8908  wunex2  9027  uniwun  9029  wuncval2  9036  grur1  9109  axgroth5  9113  axgroth2  9114  axgroth6  9117  axgroth3  9120  grothtsk  9124  inaprc  9125  ltsopi  9177  dmaddpi  9179  dmmulpi  9180  1lt2pi  9194  nqerf  9219  addnqf  9237  mulnqf  9238  1lt2nq  9262  m1p1sr  9380  m1m1sr  9381  0lt1sr  9383  axaddf  9433  axmulf  9434  ax1cn  9437  subaddrii  9822  ixi  10095  recgt0ii  10367  nn1suc  10473  neg1lt0  10559  4d2e2  10609  arch  10709  un0mulcl  10747  nummac  10927  uzf  11004  indstr  11069  mnfltpnf  11256  ixxf  11460  ioof  11543  fzf  11597  fzp1disj  11660  fzp1nel  11684  fzof  11719  om2uzrani  11966  om2uzf1oi  11967  uzrdglem  11971  uzrdgfni  11972  uzrdg0i  11973  ltwenn  11976  hashgf1o  11984  axdc4uzlem  11995  sq0  12162  irec  12170  hashkf  12309  hashf  12314  hash0  12340  prhash2ex  12368  hashsslei  12388  hashxplem  12395  hashbclem  12405  hashf1lem1  12408  wrdexg  12464  wrd0OLD  12474  revs1  12650  0csh0  12675  cshw1  12701  cats1fvn  12734  relexp0g  12859  relexpsucnnr  12862  dfrtrclrec2  12892  rtrclreclem1  12893  rtrclreclem2  12894  rtrclreclem4  12896  dfrtrcl2  12897  climmo  13382  fsumcom2  13591  ackbijnn  13642  incexclem  13650  infcvgaux1i  13670  fprodcom2  13790  efcvgfsum  13823  cos1bnd  13924  cos2bnd  13925  znnen  13948  qnnen  13949  aleph1re  13980  3dvds  14052  divalglem5  14057  bitsf  14079  sadcaddlem  14109  sadadd2lem  14111  sadadd3  14113  sadaddlem  14118  2prm  14235  phicl2  14300  pockthi  14427  unbenlem  14428  prmrec  14442  vdwlem13  14513  vdwnn  14518  ramcl2  14536  mod2xnegi  14559  modsubi  14560  structcnvcnv  14645  structfun  14646  setsres  14664  strfv  14670  strlemor1  14729  strleun  14732  0rest  14837  firest  14840  restid  14841  prdsval  14862  prdsbas  14864  prdsplusg  14865  prdsmulr  14866  prdsvsca  14867  prdsds  14871  imasaddfnlem  14935  imasvscafn  14944  oppchomfval  15120  oppcbas  15124  2oppchomf  15130  rescbas  15235  rescco  15238  rescabs  15239  0ssc  15243  0subcat  15244  idfucl  15287  wunnat  15362  homarel  15432  dmaf  15445  cdaf  15446  catcfuccl  15505  relxpchom  15567  catcxpccl  15593  oppchofcl  15646  oyoncl  15656  odubas  15880  letsr  15974  mgmidmo  16003  releqg  16365  ga0  16453  oppglem  16502  psgnunilem3  16638  psgnunilem4  16639  pmtrsn  16661  efgval  16852  efger  16853  efgsp1  16872  efgsfo  16874  efgredleme  16878  efgredlem  16882  efgred  16883  cygctb  17011  gsum2d2lem  17115  gsum2d2  17116  gsumcom2  17117  dprd2d2  17206  pgpfaclem1  17245  mgplem  17259  mgpress  17265  opprlem  17390  reldvdsr  17406  00lsp  17740  sralem  17936  srasca  17940  sravsca  17941  psrvscafval  18156  opsrbaslem  18255  psrbag0  18272  00ply1bas  18394  ply1plusgfvi  18396  xrsmgm  18566  zlmsca  18651  znbaslem  18668  resubdrg  18735  ocvfval  18788  ocv0  18799  cssval  18804  thlbas  18818  thlle  18819  islinds2  18933  matsca  19002  m2detleib  19218  eltopspOLD  19504  tgdom  19565  tgidm  19567  indistps2ALT  19600  restbas  19745  resttopon  19748  rest0  19756  leordtval2  19799  iocpnfordt  19802  icomnfordt  19803  iooordt  19804  cnpfval  19821  iscnp2  19826  ist1-3  19936  1stcfb  20031  islly2  20070  comppfsc  20118  1stckgen  20140  ptbasfi  20167  xkotf  20171  dfac14  20204  opnfbas  20428  hauspwpwf1  20573  alexsubALTlem4  20635  alexsubALT  20636  ptcmplem5  20641  cnextrel  20648  ust0  20807  tuslem  20855  0met  20954  prdsdsf  20955  prdsxmetlem  20956  prdsmet  20958  setsmsbas  21063  setsmsds  21064  prdsbl  21079  tngds  21247  qtopbaslem  21350  xrtgioo  21396  xrsdsre  21400  zcld  21403  recld2  21404  sszcld  21407  reperflem  21408  retopcon  21419  iccpnfcnv  21529  bndth  21543  ishtpy  21557  nmoleub2lem2  21684  recmet  21847  resscdrg  21883  ishl2  21895  recms  21897  volf  22025  iundisj2  22044  volsup  22051  icombl  22059  ioombl  22060  ismbf3d  22146  0plef  22164  0pledm  22165  itg1ge0  22178  mbfi1fseqlem5  22211  itg2addlem  22250  iblcnlem1  22279  reldv  22359  limciun  22383  dvexp  22441  dveflem  22465  lhop1lem  22499  lhop  22502  elply2  22678  elplyd  22684  ply1term  22686  ply0  22690  plymullem  22698  qaa  22804  pserulm  22902  pserdvlem2  22908  efcn  22923  sincosq1lem  22975  tangtx  22983  sincos4thpi  22991  sincos6thpi  22993  pige3  22995  efif1olem4  23017  logf1o  23037  relogf1o  23039  log1  23058  loge  23059  relogiso  23070  dvrelog  23105  relogcn  23106  logcn  23115  cxpcn3  23209  resqrtcn  23210  leibpi  23389  log2ublem1  23393  birthday  23401  emcllem5  23446  harmonicbnd  23450  harmonicbnd2  23451  emgt0  23453  harmonicbnd3  23454  ppiltx  23568  ppiublem1  23594  ppiub  23596  bclbnd  23672  bpos1lem  23674  bposlem8  23683  lgsquadlem2  23747  2sqlem9  23765  2sqlem10  23766  chebbnd1  23774  selberg2lem  23852  pntrsumo1  23867  selbergsb  23877  pntpbnd  23890  istrkg2ld  23975  ttgval  24299  ttglem  24300  cchhllem  24311  ax5seglem7  24359  axlowdimlem4  24369  axlowdimlem6  24371  axlowdimlem7  24372  axlowdimlem10  24375  axlowdimlem13  24378  axlowdimlem16  24381  uhgra0  24430  umgra0  24446  usgra0  24491  usgra1v  24511  cusgraexilem2  24588  cusgrasizeindslem2  24595  0wlk  24668  0trl  24669  wlkntrllem2  24683  wlkntrl  24685  0pth  24693  1pthonlem1  24712  usgrcyclnl2  24762  4cycl4dv  24788  wwlknext  24845  wwlknfi  24859  disjxwwlkn  24866  vdgrf  25019  umgrabi  25104  vdegp1ai  25105  vdegp1bi  25106  konigsberg  25108  frgra0  25115  numclwwlkdisj  25201  numclwwlk3lem  25229  ex-dif  25265  ex-in  25267  ex-eprel  25275  ex-id  25276  ex-fl  25289  avril1  25292  2bornot2b  25293  grposn  25334  issubgoi  25429  0vfval  25616  vsfval  25645  ajmoi  25891  ajfuni  25892  normlem2  26145  norm3adifii  26182  hhip  26211  hlim0  26270  hlimcaui  26271  hlimf  26272  hhssnv  26297  shscli  26352  shsval2i  26422  h1de2i  26588  fh3i  26658  fh4i  26659  cm2mi  26661  qlaxr3i  26671  mayetes3i  26764  ho0f  26786  hoif  26789  hodidi  26822  ho0subi  26830  hosd1i  26857  adjmo  26867  nmopsetn0  26900  nmfnsetn0  26913  funadj  26921  funcnvadj  26928  nmcexi  27061  cnlnadjlem8  27109  nmoptri2i  27134  opsqrlem4  27178  hmopidmchi  27186  pjoci  27215  pjinvari  27226  abrexdomjm  27523  elim2ifim  27548  iundisj2f  27579  mptexgf  27605  rinvf1o  27610  funcnvmptOLD  27655  dfcnv2  27664  snct  27683  dmct  27686  fpwrelmap  27706  iundisj2fi  27755  gsumle  27923  xrge0pluscn  28076  zlmds  28098  zlmtset  28099  qqhre  28151  esumrnmpt2  28216  esumfsup  28218  esumpcvgval  28226  hasheuni  28233  esumcvg  28234  esumcvgsum  28236  esumsup  28237  esum2d  28241  dmsigagen  28293  measvuni  28341  voliune  28357  volfiniune  28358  br2base  28396  dya2iocuni  28410  eulerpartlem1  28489  eulerpartlemt  28493  eulerpartgbij  28494  fib0  28521  coinfliprv  28604  ballotlem2  28610  ballotlemic  28628  ballotlem7  28657  ballotth  28659  plymul02  28686  lgamgulm2  28767  lgamcvglem  28771  gamf  28774  subfacp1lem5  28817  subfacp1lem6  28818  kur14lem9  28847  cvmcov2  28909  cvmliftlem1  28919  cvmliftlem4  28922  cvmliftlem5  28923  msrfo  29095  problem5  29212  ghomgrpilem2  29215  brtpid1  29264  brtpid2  29265  brtpid3  29266  logi  29287  faclimlem1  29334  domep  29390  axextndbi  29402  poseq  29498  wfrlem6  29513  wfrlem14  29521  wfrlem16  29523  frrlem10  29563  sltval2  29581  brv  29680  txprel  29682  relsset  29691  relbigcup  29700  fvbigcup  29705  fnsingle  29722  fvsingle  29723  snelsingles  29725  funimage  29731  fullfunfnv  29749  imagesset  29756  funtransport  29834  colinrel  29860  funray  29943  funline  29945  bpolylem  29963  bpoly3  29973  bpoly4  29974  0hf  29987  waj-ax  30032  lukshef-ax2  30033  arg-ax  30034  limsucncmpi  30063  mblfinlem1  30216  mblfinlem2  30217  ismblfin  30220  voliunnfl  30223  cnambfre  30228  dvtanlemOLD  30230  neibastop2lem  30344  filnetlem3  30364  cover2  30370  abrexdom  30387  fdc  30404  cncfres  30427  heibor1lem  30471  bicontr  30643  an12i  30664  tsim1  30703  ac6s6f  30747  moxfr  30790  mapfzcons1  30815  diophrw  30857  0dioph  30877  vdioph  30878  rabren3dioph  30914  2nn0ind  31046  rpnnen3  31140  kelac2lem  31176  frlmpwfi  31214  3lcm2e6  31387  lhe4.4ex1a  31402  rusbcALT  31514  ipo0  31526  ifr0  31527  fnchoice  31571  fprodn0f  31760  fprodge0  31763  fprodge1  31764  resincncf  31843  dvnprodlem3  31911  mbf0  31922  volioc  31937  stoweidlem13  31961  stoweidlem34  31982  stirlinglem5  32026  stirlinglem13  32034  stirlingr  32038  fourierdlem42  32097  fourierdlem62  32117  fouriersw  32180  etransc  32232  aistia  32258  aisfina  32259  aiffnbandciffatnotciffb  32265  axorbciffatcxorb  32266  abnotbtaxb  32277  abnotataxb  32278  0noddALTV  32531  2noddALTV  32535  pfx2  32587  usgra2pthspth  32669  usgra2pthlem1  32671  uhg0e  32694  oddinmgm  32821  2zrngamgm  32945  2zrngaabl  32950  2zrngmmgm  32952  2zrngnring  32958  fldhmsubc  33092  fldhmsubcALTV  33111  eliunxp2  33123  zlmodzxzldeplem  33299  zlmodzxzldep  33305  ldepslinc  33310  3halfnz  33326  ex-gte  33459  empty-surprise  33531  eximp-surprise2  33534  vk15.4j  33631  2sb5nd  33673  dfvd1ir  33690  dfvd2anir  33701  dfvd2ir  33703  dfvd3ir  33710  dfvd3anir  33713  iden2  33740  e0bir  33914  uun2221p1  33951  uun2221p2  33952  2sb5ndVD  34057  2sb5ndALT  34079  iunconlem2  34082  bnj226  34136  bnj1101  34190  bnj110  34263  bnj149  34280  bnj150  34281  bnj151  34282  bnj517  34290  bnj580  34318  bnj865  34328  bnj900  34334  bnj996  34360  bnj1110  34385  bnj1133  34392  bnj1128  34393  bnj1145  34396  bnj1137  34398  bnj1171  34403  bnj1176  34408  bj-babylob  34539  bj-nalnalimiOLD  34570  bj-nfv  34574  bj-dvdemo1  34735  bj-disjcsn  34853  bj-snsetex  34869  bj-0eltag  34884  bj-2upln0  34929  bj-2upln1upl  34930  elimhyps  35105  dedths  35106  renegclALT  35107  hlhilslem  38081  ifpbiidcor2  38158  eliunov2  38218  xphe  38275  xpheOLD  38276  0he  38277  he0  38279  snhesn  38281  idhe  38282  frege54cor1c  38414