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  911  mpbir3an  1170  xorexmid  1367  tru  1374  nic-mpALT  1480  nic-ax  1481  nic-axALT  1482  mpgbir  1596  nfxfr  1616  19.35ri  1658  ax6ev  1712  exan  1913  cbvex2OLD  1989  ax13  2007  euequ1  2268  moanmo  2344  moaneuOLD  2346  axi12  2430  axext2  2433  eqeltri  2538  nfcxfr  2614  neir  2653  neirr  2657  exmidneOLD  2659  nesymirOLD  2728  eqnetri  2748  nelir  2788  mprgbir  2904  vex  3081  issetri  3085  moeq  3242  cdeqi  3279  eqsstri  3495  3sstr4i  3504  rabrsn  4054  tpid1  4097  tpid2  4098  tpid3  4100  pwv  4199  uni0  4227  eqbrtri  4420  tr0  4505  trv  4506  zfrep4  4520  zfnuleu  4527  axnulALT  4528  0ex  4531  inex1  4542  0elpw  4570  axpow2  4581  axpow3  4582  pwex  4584  dvdemo1  4636  zfpair2  4641  exss  4664  moop2  4695  pwundif  4737  po0  4765  epse  4812  0elon  4881  relsnop  5053  relxp  5056  rel0  5073  relopabi  5074  eliunxp  5086  opeliunxp2  5087  dmi  5163  xpidtr  5329  xpima  5389  cnvcnv  5399  dmsn0  5415  cnvsn0  5416  funmpt  5563  funmpt2  5564  isarep2  5607  fresaunres2  5692  f0  5701  f10  5781  f1o00  5782  f1oi  5785  f1osn  5787  brprcneu  5793  opabiotafun  5862  fvopab3ig  5881  opabex  6056  eufnfv  6061  canth  6159  ncanth  6160  mpt2fun  6303  reldmmpt2  6312  ovid  6318  ovidig  6319  ovidi  6320  ovig  6323  ov3  6338  caovmo  6411  relmptopab  6419  porpss  6475  uniex2  6486  snnex  6493  tfinds2  6585  finds  6613  finds2  6615  oprabex  6676  oprabex3  6677  f1stres  6709  f2ndres  6710  relmpt2opab  6766  tpos0  6886  issmo  6920  tfrlem6  6952  tfrlem8  6954  tfrlem16  6963  tfr1a  6964  tfr1  6967  tz7.44lem1  6972  seqomlem2  7017  seqomlem3  7018  seqomlem4  7019  fnseqom  7021  0lt1o  7055  0we1  7057  eqer  7245  ecopover  7315  th3qcor  7319  mapsnf1o3  7372  ssdomg  7466  ensn1  7484  snfi  7501  xpcomf1o  7511  map2xp  7592  limensuci  7598  sdom1  7624  unblem4  7679  fidomdm  7705  marypha1lem  7795  hartogslem1  7868  hartogs  7870  card2on  7881  ruALT  7929  inf2  7941  inf3lem6  7951  infeq5i  7954  zfinf2  7960  cantnflt  7992  cantnfltOLD  8022  cantnfOLD  8035  mapfienOLD  8039  cnfcom  8045  cnfcomOLD  8053  trcl  8060  tz9.1c  8062  tc2  8074  r1funlim  8085  r1fnon  8086  karden  8214  tskwe  8232  cardprclem  8261  pm54.43  8282  r0weon  8291  iunmapdisj  8305  alephfnon  8347  alephfplem4  8389  alephfp  8390  alephval3  8392  aceq3lem  8402  kmlem2  8432  cda1dif  8457  ackbij1  8519  ackbij2lem2  8521  ackbij2  8524  infpssrlem3  8586  hsmexlem4  8710  hsmexlem5  8711  axdc3lem4  8734  ac2  8742  axac3  8745  ac6  8761  axdclem2  8801  ondomon  8839  alephsucpw  8846  pwcfsdom  8859  cfpwsdom  8860  smobeth  8862  axpowndlem3  8876  axpowndlem3OLD  8877  zfcndun  8894  zfcndpow  8895  zfcndinf  8897  zfcndac  8898  wunex2  9017  uniwun  9019  wuncval2  9026  grur1  9099  axgroth5  9103  axgroth2  9104  axgroth6  9107  axgroth3  9110  grothtsk  9114  inaprc  9115  ltsopi  9169  dmaddpi  9171  dmmulpi  9172  1lt2pi  9186  nqerf  9211  addnqf  9229  mulnqf  9230  1lt2nq  9254  m1p1sr  9371  m1m1sr  9372  0lt1sr  9374  axaddf  9424  axmulf  9425  ax1cn  9428  subaddrii  9809  ixi  10077  recgt0ii  10350  nn1suc  10455  neg1lt0  10540  4d2e2  10590  arch  10688  un0mulcl  10726  nummac  10899  uzf  10976  indstr  11035  mnfltpnf  11218  ixxf  11422  ioof  11505  fzf  11559  fzp1disj  11633  fzof  11668  om2uzrani  11893  om2uzf1oi  11894  uzrdglem  11898  uzrdgfni  11899  uzrdg0i  11900  ltwenn  11903  hashgf1o  11911  axdc4uzlem  11922  sq0  12075  irec  12083  hashkf  12223  hashf  12228  hash0  12253  hashsslei  12295  hashxplem  12314  hashbclem  12324  hashf1lem1  12327  wrdexg  12363  wrd0  12371  revs1  12524  0csh0  12549  cshw1  12575  cats1fvn  12604  climmo  13154  fsumcom2  13360  ackbijnn  13410  incexclem  13418  infcvgaux1i  13438  efcvgfsum  13490  cos1bnd  13590  cos2bnd  13591  znnen  13614  qnnen  13615  aleph1re  13646  dvdslelem  13696  3dvds  13715  divalglem5  13720  bitsf  13742  sadcaddlem  13772  sadadd2lem  13774  sadadd3  13776  sadaddlem  13781  isprm3  13891  2prm  13898  phicl2  13962  pockthi  14087  unbenlem  14088  prmrec  14102  vdwlem13  14173  vdwnn  14178  ramcl2  14196  mod2xnegi  14219  modsubi  14220  structcnvcnv  14304  structfun  14305  setsres  14321  strfv  14327  strlemor1  14385  strleun  14388  0rest  14488  firest  14491  restid  14492  prdsval  14513  prdsbas  14515  prdsplusg  14516  prdsmulr  14517  prdsvsca  14518  prdsds  14522  imasaddfnlem  14586  imasvscafn  14595  oppchomfval  14773  oppcbas  14777  2oppchomf  14783  rescbas  14862  rescco  14865  rescabs  14866  idfucl  14911  wunnat  14986  homarel  15024  dmaf  15037  cdaf  15038  catcfuccl  15097  relxpchom  15111  catcxpccl  15137  oppchofcl  15190  oyoncl  15200  odubas  15423  letsr  15517  mgmidmo  15538  releqg  15848  ga0  15936  oppglem  15985  psgnunilem3  16122  psgnunilem4  16123  pmtrsn  16145  efgval  16336  efger  16337  efgsp1  16356  efgsfo  16358  efgredleme  16362  efgredlem  16366  efgred  16367  cygctb  16490  gsum2d2lem  16588  gsum2d2  16589  gsumcom2  16590  dprd2d2  16666  pgpfaclem1  16705  mgplem  16719  mgpress  16725  opprlem  16844  reldvdsr  16860  00lsp  17186  sralem  17382  srasca  17386  sravsca  17387  psrvscafval  17585  opsrbaslem  17684  psrbag0  17701  00ply1bas  17819  ply1plusgfvi  17821  nn0srg  18007  rge0srg  18008  zlmsca  18078  znbaslem  18097  resubdrg  18164  ocvfval  18217  ocv0  18228  cssval  18233  thlbas  18247  thlle  18248  islinds2  18368  matsca  18442  m2detleib  18570  eltopspOLD  18656  tgdom  18716  tgidm  18718  indistps2ALT  18751  restbas  18895  resttopon  18898  rest0  18906  leordtval2  18949  iocpnfordt  18952  icomnfordt  18953  iooordt  18954  cnpfval  18971  iscnp2  18976  ist1-3  19086  1stcfb  19182  islly2  19221  1stckgen  19260  ptbasfi  19287  xkotf  19291  dfac14  19324  opnfbas  19548  hauspwpwf1  19693  alexsubALTlem4  19755  alexsubALT  19756  ptcmplem5  19761  cnextrel  19768  ust0  19927  tuslem  19975  0met  20074  prdsdsf  20075  prdsxmetlem  20076  prdsmet  20078  setsmsbas  20183  setsmsds  20184  prdsbl  20199  tngds  20367  qtopbaslem  20470  xrtgioo  20516  xrsdsre  20520  zcld  20523  recld2  20524  sszcld  20527  reperflem  20528  retopcon  20539  iccpnfcnv  20649  bndth  20663  ishtpy  20677  nmoleub2lem2  20804  recmet  20967  resscdrg  21003  ishl2  21015  recms  21017  ehlbase  21043  volf  21145  iundisj2  21164  volsup  21171  icombl  21179  ioombl  21180  ismbf3d  21266  0plef  21284  0pledm  21285  itg1ge0  21298  mbfi1fseqlem5  21331  itg2addlem  21370  iblcnlem1  21399  reldv  21479  limciun  21503  dvexp  21561  dveflem  21585  lhop1lem  21619  lhop  21622  elply2  21798  elplyd  21804  ply1term  21806  ply0  21810  plymullem  21818  qaa  21923  pserulm  22021  pserdvlem2  22027  efcn  22042  sincosq1lem  22093  tangtx  22101  sincos4thpi  22109  sincos6thpi  22111  pige3  22113  efif1olem4  22135  logf1o  22150  relogf1o  22152  log1  22168  loge  22169  relogiso  22180  dvrelog  22216  relogcn  22217  logcn  22226  cxpcn3  22320  resqrcn  22321  leibpi  22471  log2ublem1  22475  birthday  22482  emcllem5  22527  harmonicbnd  22531  harmonicbnd2  22532  emgt0  22534  harmonicbnd3  22535  ppiltx  22649  ppiublem1  22675  ppiub  22677  bclbnd  22753  bpos1lem  22755  bposlem8  22764  lgsquadlem2  22828  2sqlem9  22846  2sqlem10  22847  chebbnd1  22855  selberg2lem  22933  pntrsumo1  22948  selbergsb  22958  pntpbnd  22971  istrkg2ld  23056  ttgval  23274  ttglem  23275  cchhllem  23286  ax5seglem7  23334  axlowdimlem4  23344  axlowdimlem6  23346  axlowdimlem7  23347  axlowdimlem10  23350  axlowdimlem13  23353  axlowdimlem16  23356  axlowdimlem17  23357  axlowdim  23360  uhgra0  23396  umgra0  23412  usgra0  23442  usgra1v  23461  cusgraexilem2  23528  cusgrasizeindslem2  23535  0wlk  23597  0trl  23598  wlkntrllem2  23612  wlkntrl  23614  0pth  23622  1pthonlem1  23641  usgrcyclnl2  23680  4cycl4dv  23706  vdgrf  23721  umgrabi  23757  vdegp1ai  23758  vdegp1bi  23759  konigsberg  23761  ex-dif  23783  ex-in  23785  ex-eprel  23793  ex-id  23794  ex-fl  23807  avril1  23809  2bornot2b  23810  grposn  23855  issubgoi  23950  0vfval  24137  vsfval  24166  ajmoi  24412  ajfuni  24413  normlem2  24666  norm3adifii  24703  hhip  24732  hlim0  24791  hlimcaui  24792  hlimf  24793  hhssnv  24818  shscli  24873  shsval2i  24943  h1de2i  25109  fh3i  25179  fh4i  25180  cm2mi  25182  qlaxr3i  25192  mayetes3i  25286  ho0f  25308  hoif  25311  hodidi  25344  ho0subi  25352  hosd1i  25379  adjmo  25389  nmopsetn0  25422  nmfnsetn0  25435  funadj  25443  funcnvadj  25450  nmcexi  25583  cnlnadjlem8  25631  nmoptri2i  25656  opsqrlem4  25700  hmopidmchi  25708  pjoci  25737  pjinvari  25748  abrexdomjm  26041  elim2ifim  26059  iundisj2f  26084  rinvf1o  26101  funcnvmptOLD  26138  dfcnv2  26146  snct  26163  dmct  26166  fpwrelmap  26185  iundisj2fi  26227  gsumle  26392  reofld  26454  rearchi  26456  xrge0slmod  26458  xrge0iifcnv  26509  xrge0pluscn  26516  zlmds  26539  zlmtset  26540  cnzh  26545  rezh  26546  qqhre  26592  esumfsup  26665  esumpcvgval  26673  hasheuni  26680  esumcvg  26681  dmsigagen  26733  measvuni  26774  voliune  26790  volfiniune  26791  ddemeas  26797  br2base  26829  dya2iocuni  26843  oms0  26855  eulerpartlem1  26895  eulerpartlemt  26899  eulerpartgbij  26900  fib0  26927  fib6  26934  coinfliprv  27010  ballotlem2  27016  ballotlemfc0  27020  ballotlemfcc  27021  ballotlemic  27034  ballotlem7  27063  ballotth  27065  plymul02  27092  signswmnd  27103  lgamgulm2  27167  lgamcvglem  27171  gamf  27174  subfacp1lem5  27217  subfacp1lem6  27218  kur14lem9  27247  cvmcov2  27309  cvmliftlem1  27319  cvmliftlem4  27322  cvmliftlem5  27323  problem5  27447  ghomgrpilem2  27450  relexp0  27476  relexpsucr  27477  relexpsucl  27479  dfrtrclrec2  27490  rtrclreclem.refl  27491  rtrclreclem.subset  27492  rtrclreclem.min  27494  dfrtrcl2  27495  brtpid1  27522  brtpid2  27523  brtpid3  27524  fzp1nel  27542  fprodcom2  27640  faclimlem1  27694  domep  27751  axextndbi  27763  poseq  27859  wfrlem6  27874  wfrlem14  27882  wfrlem16  27884  frrlem10  27924  sltval2  27942  nosgnn0i  27945  brv  28053  txprel  28055  relsset  28064  relbigcup  28073  fvbigcup  28078  fnsingle  28095  fvsingle  28096  snelsingles  28098  funimage  28104  fullfunfnv  28122  imagesset  28129  funtransport  28207  colinrel  28233  funray  28316  funline  28318  bpolylem  28336  bpoly3  28346  bpoly4  28347  0hf  28360  waj-ax  28405  lukshef-ax2  28406  arg-ax  28407  limsucncmpi  28436  mblfinlem1  28577  mblfinlem2  28578  ismblfin  28581  voliunnfl  28584  cnambfre  28589  dvtanlem  28590  comppfsc  28728  neibastop2lem  28730  filnetlem3  28750  cover2  28756  abrexdom  28773  fdc  28790  cncfres  28813  heibor1lem  28857  bicontr  29029  an12i  29050  tsim1  29090  ac6s6f  29134  moxfr  29177  mapfzcons1  29202  diophrw  29246  0dioph  29266  vdioph  29267  rabren3dioph  29303  2nn0ind  29435  rpnnen3  29530  kelac2lem  29566  frlmpwfi  29602  lhe4.4ex1a  29752  rusbcALT  29842  ipo0  29854  ifr0  29855  fnchoice  29900  stoweidlem13  29957  stoweidlem34  29978  stirlinglem5  30022  stirlinglem13  30030  stirlingr  30034  aistia  30060  aisfina  30061  aiffnbandciffatnotciffb  30067  axorbciffatcxorb  30068  abnotbtaxb  30079  abnotataxb  30080  usgra2pthspth  30444  usgra2pthlem1  30449  wwlknext  30505  wwlknfi  30519  disjxwwlkn  30713  frgra0  30735  numclwwlkdisj  30822  numclwwlk3lem  30850  eliunxp2  30870  zlmodzxzldeplem  31173  zlmodzxzldep  31179  ldepslinc  31184  ex-gte  31393  AnelBC  31428  empty-surprise  31467  eximp-surprise2  31470  vk15.4j  31566  2sb5nd  31602  dfvd1ir  31619  dfvd2anir  31630  dfvd2ir  31632  dfvd3ir  31639  dfvd3anir  31642  iden2  31669  e0bir  31843  uun2221p1  31880  uun2221p2  31881  2sb5ndVD  31979  2sb5ndALT  32001  iunconlem2  32004  bnj226  32058  bnj1101  32111  bnj110  32184  bnj149  32201  bnj150  32202  bnj151  32203  bnj517  32211  bnj580  32239  bnj865  32249  bnj900  32255  bnj996  32281  bnj1110  32306  bnj1133  32313  bnj1128  32314  bnj1145  32317  bnj1137  32319  bnj1171  32324  bnj1176  32329  bj-babylob  32457  bj-nfv  32496  bj-nalnalimiOLD  32499  bj-dvdemo1  32656  bj-disjcsn  32773  bj-snsetex  32789  bj-0eltag  32804  bj-2upln0  32849  bj-2upln1upl  32850  elimhyps  32951  dedths  32952  renegclALT  32953  hlhilslem  35925