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  920  mpbir3an  1179  xorexmid  1380  tru  1387  nic-mpALT  1492  nic-ax  1493  nic-axALT  1494  mpgbir  1609  nfxfr  1632  19.35ri  1677  ax5e  1693  ax6ev  1736  exan  1959  cbvex2OLD  2015  ax13  2033  euequ1  2274  moanmo  2339  axi12  2419  axext2  2422  eqeltri  2527  nfcxfr  2603  neir  2643  neirr  2647  exmidneOLD  2649  nesymirOLD  2719  eqnetri  2739  nelir  2779  mprgbir  2807  vex  3098  issetri  3102  moeq  3261  cdeqi  3298  eqsstri  3519  3sstr4i  3528  rabrsn  4085  tpid1  4128  tpid2  4129  tpid3  4131  pwv  4233  uni0  4261  eqbrtri  4456  tr0  4541  trv  4542  zfrep4  4556  zfnuleu  4563  axnulALT  4564  0ex  4567  inex1  4578  0elpw  4606  axpow2  4617  axpow3  4618  pwex  4620  dvdemo1  4672  zfpair2  4677  exss  4700  moop2  4732  pwundif  4777  po0  4805  epse  4852  0elon  4921  relsnop  5097  relxp  5100  rel0  5117  relopabi  5118  eliunxp  5130  opeliunxp2  5131  dmi  5207  xpidtr  5379  xpima  5439  cnvcnv  5449  dmsn0  5465  cnvsn0  5466  funmpt  5614  funmpt2  5615  isarep2  5658  fresaunres2  5747  f0  5756  f10  5837  f1o00  5838  f1oi  5841  f1osn  5843  brprcneu  5849  opabiotafun  5919  fvopab3ig  5938  opabex  6126  eufnfv  6131  canth  6239  ncanth  6240  mpt2fun  6389  reldmmpt2  6398  ovid  6404  ovidig  6405  ovidi  6406  ovig  6409  ov3  6424  caovmo  6497  relmptopab  6508  porpss  6569  uniex2  6580  snnex  6591  tfinds2  6683  finds  6711  finds2  6713  oprabex  6773  oprabex3  6774  f1stres  6807  f2ndres  6808  relmpt2opab  6867  tpos0  6987  issmo  7021  tfrlem6  7053  tfrlem8  7055  tfrlem16  7064  tfr1a  7065  tfr1  7068  tz7.44lem1  7073  seqomlem2  7118  seqomlem3  7119  seqomlem4  7120  fnseqom  7122  0lt1o  7156  0we1  7158  eqer  7346  ecopover  7417  mapsnf1o3  7469  ssdomg  7563  ensn1  7581  snfi  7598  xpcomf1o  7608  map2xp  7689  limensuci  7695  sdom1  7721  unblem4  7777  fidomdm  7804  marypha1lem  7895  hartogslem1  7970  hartogs  7972  card2on  7983  ruALT  8031  inf2  8043  inf3lem6  8053  infeq5i  8056  zfinf2  8062  cantnflt  8094  cantnfltOLD  8124  cantnfOLD  8137  mapfienOLD  8141  cnfcom  8147  cnfcomOLD  8155  trcl  8162  tz9.1c  8164  tc2  8176  r1funlim  8187  r1fnon  8188  karden  8316  tskwe  8334  cardprclem  8363  pm54.43  8384  r0weon  8393  iunmapdisj  8407  alephfnon  8449  alephfplem4  8491  alephfp  8492  alephval3  8494  aceq3lem  8504  kmlem2  8534  cda1dif  8559  ackbij1  8621  ackbij2lem2  8623  ackbij2  8626  infpssrlem3  8688  hsmexlem4  8812  hsmexlem5  8813  axdc3lem4  8836  ac2  8844  axac3  8847  ac6  8863  axdclem2  8903  ondomon  8941  alephsucpw  8948  pwcfsdom  8961  cfpwsdom  8962  smobeth  8964  axpowndlem3  8978  axpowndlem3OLD  8979  zfcndun  8996  zfcndpow  8997  zfcndinf  8999  zfcndac  9000  wunex2  9119  uniwun  9121  wuncval2  9128  grur1  9201  axgroth5  9205  axgroth2  9206  axgroth6  9209  axgroth3  9212  grothtsk  9216  inaprc  9217  ltsopi  9269  dmaddpi  9271  dmmulpi  9272  1lt2pi  9286  nqerf  9311  addnqf  9329  mulnqf  9330  1lt2nq  9354  m1p1sr  9472  m1m1sr  9473  0lt1sr  9475  axaddf  9525  axmulf  9526  ax1cn  9529  subaddrii  9914  ixi  10184  recgt0ii  10457  nn1suc  10563  neg1lt0  10648  4d2e2  10698  arch  10798  un0mulcl  10836  nummac  11016  uzf  11093  indstr  11159  mnfltpnf  11344  ixxf  11548  ioof  11631  fzf  11685  fzp1disj  11747  fzof  11805  om2uzrani  12042  om2uzf1oi  12043  uzrdglem  12047  uzrdgfni  12048  uzrdg0i  12049  ltwenn  12052  hashgf1o  12060  axdc4uzlem  12071  sq0  12238  irec  12246  hashkf  12386  hashf  12391  hash0  12416  prhash2ex  12443  hashsslei  12463  hashxplem  12470  hashbclem  12480  hashf1lem1  12483  wrdexg  12536  wrd0  12544  revs1  12718  0csh0  12743  cshw1  12769  cats1fvn  12802  climmo  13359  fsumcom2  13568  ackbijnn  13619  incexclem  13627  infcvgaux1i  13647  efcvgfsum  13699  cos1bnd  13799  cos2bnd  13800  znnen  13823  qnnen  13824  aleph1re  13855  3dvds  13927  divalglem5  13932  bitsf  13954  sadcaddlem  13984  sadadd2lem  13986  sadadd3  13988  sadaddlem  13993  2prm  14110  phicl2  14175  pockthi  14302  unbenlem  14303  prmrec  14317  vdwlem13  14388  vdwnn  14393  ramcl2  14411  mod2xnegi  14434  modsubi  14435  structcnvcnv  14520  structfun  14521  setsres  14537  strfv  14543  strlemor1  14601  strleun  14604  0rest  14704  firest  14707  restid  14708  prdsval  14729  prdsbas  14731  prdsplusg  14732  prdsmulr  14733  prdsvsca  14734  prdsds  14738  imasaddfnlem  14802  imasvscafn  14811  oppchomfval  14986  oppcbas  14990  2oppchomf  14996  rescbas  15075  rescco  15078  rescabs  15079  idfucl  15124  wunnat  15199  homarel  15237  dmaf  15250  cdaf  15251  catcfuccl  15310  relxpchom  15324  catcxpccl  15350  oppchofcl  15403  oyoncl  15413  odubas  15637  letsr  15731  mgmidmo  15760  releqg  16122  ga0  16210  oppglem  16259  psgnunilem3  16395  psgnunilem4  16396  pmtrsn  16418  efgval  16609  efger  16610  efgsp1  16629  efgsfo  16631  efgredleme  16635  efgredlem  16639  efgred  16640  cygctb  16768  gsum2d2lem  16875  gsum2d2  16876  gsumcom2  16877  dprd2d2  16967  pgpfaclem1  17006  mgplem  17020  mgpress  17026  opprlem  17151  reldvdsr  17167  00lsp  17501  sralem  17697  srasca  17701  sravsca  17702  psrvscafval  17917  opsrbaslem  18016  psrbag0  18033  00ply1bas  18155  ply1plusgfvi  18157  xrsmgm  18327  zlmsca  18431  znbaslem  18450  resubdrg  18517  ocvfval  18570  ocv0  18581  cssval  18586  thlbas  18600  thlle  18601  islinds2  18721  matsca  18790  m2detleib  19006  eltopspOLD  19292  tgdom  19353  tgidm  19355  indistps2ALT  19388  restbas  19532  resttopon  19535  rest0  19543  leordtval2  19586  iocpnfordt  19589  icomnfordt  19590  iooordt  19591  cnpfval  19608  iscnp2  19613  ist1-3  19723  1stcfb  19819  islly2  19858  comppfsc  19906  1stckgen  19928  ptbasfi  19955  xkotf  19959  dfac14  19992  opnfbas  20216  hauspwpwf1  20361  alexsubALTlem4  20423  alexsubALT  20424  ptcmplem5  20429  cnextrel  20436  ust0  20595  tuslem  20643  0met  20742  prdsdsf  20743  prdsxmetlem  20744  prdsmet  20746  setsmsbas  20851  setsmsds  20852  prdsbl  20867  tngds  21035  qtopbaslem  21138  xrtgioo  21184  xrsdsre  21188  zcld  21191  recld2  21192  sszcld  21195  reperflem  21196  retopcon  21207  iccpnfcnv  21317  bndth  21331  ishtpy  21345  nmoleub2lem2  21472  recmet  21635  resscdrg  21671  ishl2  21683  recms  21685  volf  21813  iundisj2  21832  volsup  21839  icombl  21847  ioombl  21848  ismbf3d  21934  0plef  21952  0pledm  21953  itg1ge0  21966  mbfi1fseqlem5  21999  itg2addlem  22038  iblcnlem1  22067  reldv  22147  limciun  22171  dvexp  22229  dveflem  22253  lhop1lem  22287  lhop  22290  elply2  22466  elplyd  22472  ply1term  22474  ply0  22478  plymullem  22486  qaa  22591  pserulm  22689  pserdvlem2  22695  efcn  22710  sincosq1lem  22762  tangtx  22770  sincos4thpi  22778  sincos6thpi  22780  pige3  22782  efif1olem4  22804  logf1o  22824  relogf1o  22826  log1  22842  loge  22843  relogiso  22854  dvrelog  22890  relogcn  22891  logcn  22900  cxpcn3  22994  resqrtcn  22995  leibpi  23145  log2ublem1  23149  birthday  23156  emcllem5  23201  harmonicbnd  23205  harmonicbnd2  23206  emgt0  23208  harmonicbnd3  23209  ppiltx  23323  ppiublem1  23349  ppiub  23351  bclbnd  23427  bpos1lem  23429  bposlem8  23438  lgsquadlem2  23502  2sqlem9  23520  2sqlem10  23521  chebbnd1  23529  selberg2lem  23607  pntrsumo1  23622  selbergsb  23632  pntpbnd  23645  istrkg2ld  23730  ttgval  24050  ttglem  24051  cchhllem  24062  ax5seglem7  24110  axlowdimlem4  24120  axlowdimlem6  24122  axlowdimlem7  24123  axlowdimlem10  24126  axlowdimlem13  24129  axlowdimlem16  24132  uhgra0  24181  umgra0  24197  usgra0  24242  usgra1v  24262  cusgraexilem2  24339  cusgrasizeindslem2  24346  0wlk  24419  0trl  24420  wlkntrllem2  24434  wlkntrl  24436  0pth  24444  1pthonlem1  24463  usgrcyclnl2  24513  4cycl4dv  24539  wwlknext  24596  wwlknfi  24610  disjxwwlkn  24617  vdgrf  24770  umgrabi  24855  vdegp1ai  24856  vdegp1bi  24857  konigsberg  24859  frgra0  24866  numclwwlkdisj  24952  numclwwlk3lem  24980  ex-dif  25016  ex-in  25018  ex-eprel  25026  ex-id  25027  ex-fl  25040  avril1  25043  2bornot2b  25044  grposn  25089  issubgoi  25184  0vfval  25371  vsfval  25400  ajmoi  25646  ajfuni  25647  normlem2  25900  norm3adifii  25937  hhip  25966  hlim0  26025  hlimcaui  26026  hlimf  26027  hhssnv  26052  shscli  26107  shsval2i  26177  h1de2i  26343  fh3i  26413  fh4i  26414  cm2mi  26416  qlaxr3i  26426  mayetes3i  26520  ho0f  26542  hoif  26545  hodidi  26578  ho0subi  26586  hosd1i  26613  adjmo  26623  nmopsetn0  26656  nmfnsetn0  26669  funadj  26677  funcnvadj  26684  nmcexi  26817  cnlnadjlem8  26865  nmoptri2i  26890  opsqrlem4  26934  hmopidmchi  26942  pjoci  26971  pjinvari  26982  abrexdomjm  27277  elim2ifim  27295  iundisj2f  27321  rinvf1o  27344  funcnvmptOLD  27381  dfcnv2  27389  snct  27406  dmct  27409  fpwrelmap  27428  iundisj2fi  27474  gsumle  27643  xrge0pluscn  27795  zlmds  27818  zlmtset  27819  qqhre  27871  esumfsup  27949  esumpcvgval  27957  hasheuni  27964  esumcvg  27965  dmsigagen  28017  measvuni  28058  voliune  28074  volfiniune  28075  br2base  28113  dya2iocuni  28127  oms0  28139  eulerpartlem1  28179  eulerpartlemt  28183  eulerpartgbij  28184  fib0  28211  coinfliprv  28294  ballotlem2  28300  ballotlemic  28318  ballotlem7  28347  ballotth  28349  plymul02  28376  lgamgulm2  28451  lgamcvglem  28455  gamf  28458  subfacp1lem5  28501  subfacp1lem6  28502  kur14lem9  28531  cvmcov2  28593  cvmliftlem1  28603  cvmliftlem4  28606  cvmliftlem5  28607  msrfo  28779  problem5  28896  ghomgrpilem2  28899  relexp0  28925  relexpsucr  28926  relexpsucl  28928  dfrtrclrec2  28939  rtrclreclem.refl  28940  rtrclreclem.subset  28941  rtrclreclem.min  28943  dfrtrcl2  28944  brtpid1  28971  brtpid2  28972  brtpid3  28973  fzp1nel  28991  fprodcom2  29089  faclimlem1  29143  domep  29200  axextndbi  29212  poseq  29308  wfrlem6  29323  wfrlem14  29331  wfrlem16  29333  frrlem10  29373  sltval2  29391  brv  29502  txprel  29504  relsset  29513  relbigcup  29522  fvbigcup  29527  fnsingle  29544  fvsingle  29545  snelsingles  29547  funimage  29553  fullfunfnv  29571  imagesset  29578  funtransport  29656  colinrel  29682  funray  29765  funline  29767  bpolylem  29785  bpoly3  29795  bpoly4  29796  0hf  29809  waj-ax  29854  lukshef-ax2  29855  arg-ax  29856  limsucncmpi  29885  mblfinlem1  30026  mblfinlem2  30027  ismblfin  30030  voliunnfl  30033  cnambfre  30038  dvtanlem  30039  neibastop2lem  30153  filnetlem3  30173  cover2  30179  abrexdom  30196  fdc  30213  cncfres  30236  heibor1lem  30280  bicontr  30452  an12i  30473  tsim1  30512  ac6s6f  30556  moxfr  30599  mapfzcons1  30624  diophrw  30667  0dioph  30687  vdioph  30688  rabren3dioph  30724  2nn0ind  30856  rpnnen3  30949  kelac2lem  30985  frlmpwfi  31021  3lcm2e6  31195  lhe4.4ex1a  31210  rusbcALT  31300  ipo0  31312  ifr0  31313  fnchoice  31358  resincncf  31584  mbf0  31646  volioc  31661  stoweidlem13  31684  stoweidlem34  31705  stirlinglem5  31749  stirlinglem13  31757  stirlingr  31761  fourierdlem42  31820  fourierdlem62  31840  fouriersw  31903  aistia  31930  aisfina  31931  aiffnbandciffatnotciffb  31937  axorbciffatcxorb  31938  abnotbtaxb  31949  abnotataxb  31950  usgra2pthspth  32189  usgra2pthlem1  32191  uhg0e  32214  oddinmgm  32340  2zrngamgm  32455  2zrngaabl  32460  2zrngmmgm  32462  2zrngnring  32468  fldhmsubc  32625  fldhmsubcOLD  32644  eliunxp2  32656  zlmodzxzldeplem  32834  zlmodzxzldep  32840  ldepslinc  32845  ex-gte  32858  empty-surprise  32932  eximp-surprise2  32935  vk15.4j  33031  2sb5nd  33066  dfvd1ir  33083  dfvd2anir  33094  dfvd2ir  33096  dfvd3ir  33103  dfvd3anir  33106  iden2  33133  e0bir  33307  uun2221p1  33344  uun2221p2  33345  2sb5ndVD  33443  2sb5ndALT  33465  iunconlem2  33468  bnj226  33522  bnj1101  33576  bnj110  33649  bnj149  33666  bnj150  33667  bnj151  33668  bnj517  33676  bnj580  33704  bnj865  33714  bnj900  33720  bnj996  33746  bnj1110  33771  bnj1133  33778  bnj1128  33779  bnj1145  33782  bnj1137  33784  bnj1171  33789  bnj1176  33794  bj-babylob  33940  bj-nalnalimiOLD  33971  bj-nfv  33975  bj-dvdemo1  34136  bj-disjcsn  34253  bj-snsetex  34269  bj-0eltag  34284  bj-2upln0  34329  bj-2upln1upl  34330  elimhyps  34432  dedths  34433  renegclALT  34434  hlhilslem  37408  xphe  37491  0he  37492  he0  37494  snhesn  37496  idhe  37497  frege54cor1c  37611