Theorem mpbir 212

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 209	. 2 |- ( ps -> ph )
4	1, 3	ax-mp 5	1 |- ph

Syntax hints:   <-> wb 187

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 188

This theorem is referenced by:  pm5.74ri  249  con4bii  298  orri  377  imorri  415  imnani  424  mpbir2an  928  mpbir3an  1187  xorexmid  1419  tru  1441  had1  1499  nic-mpALT  1549  nic-ax  1550  nic-axALT  1551  mpgbir  1667  nfxfr  1690  19.35ri  1736  ax5e  1754  ax6ev  1800  exan  2032  ax13  2106  euequ1  2275  moanmo  2331  axi12  2399  axext2  2402  eqeltri  2503  nfcxfr  2578  neir  2619  neirr  2624  exmidneOLD  2626  nesymirOLD  2696  eqnetri  2716  nelir  2757  mprgbir  2786  vex  3083  issetri  3087  moeq  3246  rmoeq  3269  cdeqi  3284  eqsstri  3494  3sstr4i  3503  rabrsn  4070  tpid1  4113  tpid2  4114  tpid3  4116  pwv  4218  uni0  4246  eqbrtri  4443  tr0  4529  trv  4530  zfrep4  4544  zfnuleu  4551  axnulALT  4552  0ex  4556  inex1  4565  0elpw  4593  axpow2  4604  axpow3  4605  pwex  4607  dvdemo1  4656  zfpair2  4661  exss  4684  moop2  4715  pwundif  4760  po0  4789  epse  4836  relsnop  4958  relxp  4961  rel0  4977  relopabi  4978  eliunxp  4991  opeliunxp2  4992  dmi  5068  xpidtr  5241  xpima  5298  cnvcnv  5307  dmsn0  5322  cnvsn0  5323  0elon  5495  funmpt  5637  funmpt2  5638  isarep2  5681  fresaunres2  5772  f0  5781  f10  5862  f1o00  5863  f1oi  5866  f1osn  5868  brprcneu  5874  opabiotafun  5942  fvopab3ig  5961  opabex  6149  eufnfv  6154  canth  6264  ncanth  6265  mpt2fun  6412  reldmmpt2  6421  ovid  6427  ovidig  6428  ovidi  6429  ovig  6432  ov3  6447  caovmo  6520  relmptopab  6531  porpss  6589  uniex2  6600  snnex  6611  tfinds2  6704  finds  6733  finds2  6735  oprabex  6795  oprabex3  6796  f1stres  6829  f2ndres  6830  relmpt2opab  6889  opeliunxp2f  6967  tpos0  7014  wfrrel  7052  wfrlem14  7060  wfrlem16  7062  issmo  7078  tfrlem6  7111  tfrlem8  7113  tfrlem16  7122  tfr1a  7123  tfr1  7126  tz7.44lem1  7134  seqomlem2  7179  seqomlem3  7180  seqomlem4  7181  fnseqom  7183  0lt1o  7217  0we1  7219  eqer  7407  ecopover  7478  mapsnf1o3  7531  ssdomg  7625  ensn1  7643  snfi  7660  xpcomf1o  7670  map2xp  7751  limensuci  7757  sdom1  7781  unblem4  7835  fidomdm  7862  marypha1lem  7956  hartogslem1  8066  hartogs  8068  card2on  8078  ruALT  8125  inf2  8137  inf3lem6  8147  infeq5i  8150  zfinf2  8156  cantnflt  8185  cnfcom  8213  trcl  8220  tz9.1c  8222  tc2  8234  r1funlim  8245  r1fnon  8246  karden  8374  tskwe  8392  cardprclem  8421  pm54.43  8442  r0weon  8451  iunmapdisj  8461  alephfnon  8503  alephfplem4  8545  alephfp  8546  alephval3  8548  aceq3lem  8558  kmlem2  8588  cda1dif  8613  ackbij1  8675  ackbij2lem2  8677  ackbij2  8680  infpssrlem3  8742  hsmexlem4  8866  hsmexlem5  8867  axdc3lem4  8890  ac2  8898  axac3  8901  ac6  8917  axdclem2  8957  ondomon  8995  alephsucpw  9002  pwcfsdom  9015  cfpwsdom  9016  smobeth  9018  axpowndlem3  9031  zfcndun  9047  zfcndpow  9048  zfcndinf  9050  zfcndac  9051  wunex2  9170  uniwun  9172  wuncval2  9179  grur1  9252  axgroth5  9256  axgroth2  9257  axgroth6  9260  axgroth3  9263  grothtsk  9267  inaprc  9268  ltsopi  9320  dmaddpi  9322  dmmulpi  9323  1lt2pi  9337  nqerf  9362  addnqf  9380  mulnqf  9381  1lt2nq  9405  m1p1sr  9523  m1m1sr  9524  0lt1sr  9526  axaddf  9576  axmulf  9577  ax1cn  9580  subaddrii  9971  ixi  10248  recgt0ii  10519  nn1suc  10637  neg1lt0  10723  4d2e2  10773  arch  10873  un0mulcl  10911  nummac  11090  uzf  11169  indstr  11234  mnfltpnf  11435  ixxf  11652  ioof  11739  fzf  11795  0nelfz1  11825  fzp1disj  11861  fzp1nel  11885  fzof  11924  om2uzrani  12172  om2uzf1oi  12173  uzrdglem  12177  uzrdgfni  12178  uzrdg0i  12179  ltwenn  12182  hashgf1o  12190  axdc4uzlem  12201  sq0  12372  irec  12380  facmapnn  12476  hashkf  12523  hashf  12528  hash0  12554  prhash2ex  12582  hashsslei  12602  hashxplem  12609  hashbclem  12619  hashf1lem1  12622  wrdexg  12686  wrd0OLD  12696  revs1  12872  0csh0  12897  cshw1  12923  cats1fvn  12956  relexp0g  13085  relexpsucnnr  13088  dfrtrclrec2  13120  rtrclreclem1  13121  rtrclreclem2  13122  rtrclreclem4  13124  dfrtrcl2  13125  climmo  13620  fsumcom2  13834  ackbijnn  13885  incexclem  13893  infcvgaux1i  13914  fprodcom2  14037  fprodn0f  14044  fprodge0  14046  fprodge1  14048  bpolylem  14100  bpoly3  14110  bpoly4  14111  efcvgfsum  14139  cos1bnd  14240  cos2bnd  14241  znnen  14264  qnnen  14265  aleph1re  14296  3dvds  14368  divalglem5OLD  14375  divalglem5  14376  bitsf  14399  sadcaddlem  14430  sadadd2lem  14432  sadadd3  14434  sadaddlem  14439  lcmf0  14606  lcmfunsnlem2lem1  14610  lcmfunsnlem2  14612  2prm  14639  coprmprod  14677  coprmproddvdslem  14678  3lcm2e6  14680  phicl2  14715  pockthi  14850  unbenlem  14851  prmrec  14865  vdwlem13  14942  vdwnn  14947  ramcl2  14972  ramcl2OLD  14973  lcmsmapnnOLD  15010  prmormapnnOLD  15013  prmgapprmo  15032  mod2xnegi  15042  modsubi  15043  prmo4  15098  prmo5  15099  prmo6  15100  structcnvcnv  15131  structfun  15132  setsres  15150  strfv  15156  strlemor1  15216  strleun  15219  0rest  15327  firest  15330  restid  15331  prdsval  15352  prdsbas  15354  prdsplusg  15355  prdsmulr  15356  prdsvsca  15357  prdsds  15361  imasaddfnlem  15433  imasvscafn  15442  oppchomfval  15618  oppcbas  15622  2oppchomf  15628  rescbas  15733  rescco  15736  rescabs  15737  0ssc  15741  0subcat  15742  idfucl  15785  wunnat  15860  homarel  15930  dmaf  15943  cdaf  15944  catcfuccl  16003  relxpchom  16065  catcxpccl  16091  oppchofcl  16144  oyoncl  16154  odubas  16378  letsr  16472  mgmidmo  16501  releqg  16863  ga0  16951  oppglem  17000  psgnunilem3  17136  psgnunilem4  17137  pmtrsn  17159  efgval  17366  efger  17367  efgsp1  17386  efgsfo  17388  efgredleme  17392  efgredlem  17396  efgred  17397  cygctb  17525  gsum2d2lem  17604  gsum2d2  17605  gsumcom2  17606  dprd2d2  17676  pgpfaclem1  17713  mgplem  17727  mgpress  17733  opprlem  17855  reldvdsr  17871  00lsp  18203  sralem  18399  srasca  18403  sravsca  18404  psrvscafval  18613  opsrbaslem  18700  psrbag0  18716  00ply1bas  18832  ply1plusgfvi  18834  xrsmgm  19002  zlmsca  19090  znbaslem  19107  resubdrg  19174  ocvfval  19227  ocv0  19238  cssval  19243  thlbas  19257  thlle  19258  islinds2  19369  matsca  19438  m2detleib  19654  tgdom  19992  tgidm  19994  indistps2ALT  20027  restbas  20172  resttopon  20175  rest0  20183  leordtval2  20226  iocpnfordt  20229  icomnfordt  20230  iooordt  20231  cnpfval  20248  iscnp2  20253  ist1-3  20363  1stcfb  20458  islly2  20497  comppfsc  20545  1stckgen  20567  ptbasfi  20594  xkotf  20598  dfac14  20631  opnfbas  20855  hauspwpwf1  21000  alexsubALTlem4  21063  alexsubALT  21064  ptcmplem5  21069  cnextrel  21076  ust0  21232  tuslem  21280  0met  21379  prdsdsf  21380  prdsxmetlem  21381  prdsmet  21383  setsmsbas  21488  setsmsds  21489  prdsbl  21504  tngds  21654  qtopbaslem  21777  xrtgioo  21822  xrsdsre  21826  zcld  21829  recld2  21830  sszcld  21833  reperflem  21834  retopcon  21845  iccpnfcnv  21970  bndth  21984  ishtpy  22001  nmoleub2lem2  22128  recmet  22289  resscdrg  22323  ishl2  22335  recms  22337  volf  22481  iundisj2  22500  volsup  22507  icombl  22515  ioombl  22516  ismbf3d  22608  0plef  22628  0pledm  22629  itg1ge0  22642  mbfi1fseqlem5  22675  itg2addlem  22714  iblcnlem1  22743  reldv  22823  limciun  22847  dvexp  22905  dveflem  22929  lhop1lem  22963  lhop  22966  elply2  23148  elplyd  23154  ply1term  23156  ply0  23160  plymullem  23168  qaa  23277  pserulm  23375  pserdvlem2  23381  efcn  23396  sincosq1lem  23450  tangtx  23458  sincos4thpi  23466  sincos6thpi  23468  pige3  23470  efif1olem4  23492  logf1o  23512  relogf1o  23514  log1  23533  loge  23534  relogiso  23545  dvrelog  23580  relogcn  23581  logcn  23590  cxpcn3  23686  resqrtcn  23687  leibpi  23866  log2ublem1  23870  birthday  23878  emcllem5  23923  harmonicbnd  23927  harmonicbnd2  23928  emgt0  23930  harmonicbnd3  23931  lgamgulm2  23959  lgamcvglem  23963  gamf  23966  ppiltx  24102  ppiublem1  24128  ppiub  24130  bclbnd  24206  bpos1lem  24208  bposlem8  24217  lgsquadlem2  24281  2sqlem9  24299  2sqlem10  24300  chebbnd1  24308  selberg2lem  24386  pntrsumo1  24401  selbergsb  24411  pntpbnd  24424  istrkg2ld  24506  tgcgr4  24574  ttgval  24903  ttglem  24904  cchhllem  24915  ax5seglem7  24963  axlowdimlem4  24973  axlowdimlem6  24975  axlowdimlem7  24976  axlowdimlem10  24979  axlowdimlem13  24982  axlowdimlem16  24985  uhgra0  25034  umgra0  25050  usgra0  25095  usgra1v  25115  cusgraexilem2  25193  cusgrasizeindslem2  25200  0wlk  25273  0trl  25274  wlkntrllem2  25288  wlkntrl  25290  0pth  25298  1pthonlem1  25317  usgrcyclnl2  25367  4cycl4dv  25393  wwlknext  25450  wwlknfi  25464  disjxwwlkn  25471  vdgrf  25624  umgrabi  25709  vdegp1ai  25710  vdegp1bi  25711  konigsberg  25713  frgra0  25720  numclwwlkdisj  25806  numclwwlk3lem  25834  ex-dif  25871  ex-in  25873  ex-eprel  25881  ex-id  25882  ex-fl  25895  avril1  25898  2bornot2b  25899  grposn  25941  issubgoi  26036  0vfval  26223  vsfval  26252  ajmoi  26498  ajfuni  26499  normlem2  26762  norm3adifii  26799  hhip  26828  hlim0  26886  hlimcaui  26887  hlimf  26888  hhssnv  26913  shscli  26968  shsval2i  27038  h1de2i  27204  fh3i  27274  fh4i  27275  cm2mi  27277  qlaxr3i  27287  mayetes3i  27380  ho0f  27402  hoif  27405  hodidi  27438  ho0subi  27446  hosd1i  27473  adjmo  27483  nmopsetn0  27516  nmfnsetn0  27529  funadj  27537  funcnvadj  27544  nmcexi  27677  cnlnadjlem8  27725  nmoptri2i  27750  opsqrlem4  27794  hmopidmchi  27802  pjoci  27831  pjinvari  27842  abrexdomjm  28140  elim2ifim  28164  iundisj2f  28202  mptexgf  28227  rinvf1o  28232  funcnvmptOLD  28272  dfcnv2  28281  snct  28301  dmct  28304  fpwrelmap  28324  iundisj2fi  28379  gsumle  28549  xrge0slmod  28615  xrge0pluscn  28754  zlmds  28776  zlmtset  28777  qqhre  28832  esumrnmpt2  28897  esumfsup  28899  esumpcvgval  28907  hasheuni  28914  esumcvg  28915  esumcvgsum  28917  esumsup  28918  esum2d  28922  dmsigagen  28974  ldgenpisyslem3  28995  measvuni  29044  voliune  29060  volfiniune  29061  br2base  29099  dya2iocuni  29113  eulerpartlem1  29208  eulerpartlemt  29212  eulerpartgbij  29213  fib0  29240  coinfliprv  29323  ballotlem2  29329  ballotlemic  29347  ballotlem7  29376  ballotth  29378  ballotlemicOLD  29385  ballotlem7OLD  29414  ballotthOLD  29416  plymul02  29443  bnj226  29550  bnj1101  29604  bnj110  29677  bnj149  29694  bnj150  29695  bnj151  29696  bnj517  29704  bnj580  29732  bnj865  29742  bnj900  29748  bnj996  29774  bnj1110  29799  bnj1133  29806  bnj1128  29807  bnj1145  29810  bnj1137  29812  bnj1171  29817  bnj1176  29822  subfacp1lem5  29915  subfacp1lem6  29916  kur14lem9  29945  cvmcov2  30006  cvmliftlem1  30016  cvmliftlem4  30019  cvmliftlem5  30020  msrfo  30192  problem5  30309  ghomgrpilem2  30312  brtpid1  30361  brtpid2  30362  brtpid3  30363  logi  30377  faclimlem1  30386  domep  30446  axextndbi  30458  poseq  30498  frrlem10  30532  sltval2  30550  brv  30649  txprel  30651  relsset  30660  relbigcup  30669  fvbigcup  30674  fnsingle  30691  fvsingle  30692  snelsingles  30694  funimage  30700  fullfunfnv  30718  imagesset  30725  funtransport  30803  colinrel  30829  funray  30912  funline  30914  0hf  30949  neibastop2lem  31021  filnetlem3  31041  waj-ax  31079  lukshef-ax2  31080  arg-ax  31081  limsucncmpi  31110  bj-babylob  31191  bj-nalnalimiOLD  31222  bj-nfv  31226  bj-dvdemo1  31387  bj-disjcsn  31510  bj-snsetex  31525  bj-0eltag  31540  bj-2upln0  31585  bj-2upln1upl  31586  f1omptsnlem  31702  f1omptsn  31703  icoreresf  31719  relowlssretop  31730  relowlpssretop  31731  pigt3  31902  poimirlem3  31907  poimirlem9  31913  poimirlem16  31920  poimirlem17  31921  poimirlem18  31922  poimirlem19  31923  poimirlem20  31924  poimirlem26  31930  mblfinlem1  31941  mblfinlem2  31942  ismblfin  31945  voliunnfl  31948  cnambfre  31953  dvtanlemOLD  31955  cover2  32004  abrexdom  32021  fdc  32038  cncfres  32061  heibor1lem  32105  bicontr  32277  an12i  32298  tsim1  32336  ac6s6f  32380  elimhyps  32502  dedths  32503  renegclALT  32504  hlhilslem  35478  moxfr  35503  mapfzcons1  35528  diophrw  35570  0dioph  35590  vdioph  35591  rabren3dioph  35627  2nn0ind  35763  rpnnen3  35857  kelac2lem  35892  frlmpwfi  35926  ifpbiidcor2  36097  relintabex  36157  eliunov2  36241  xphe  36346  xpheOLD  36347  0he  36348  he0  36350  snhesn  36352  idhe  36353  frege54cor1c  36481  amgm2d  36620  amgm3d  36621  amgm4d  36622  lhe4.4ex1a  36648  rusbcALT  36760  ipo0  36772  ifr0  36773  vk15.4j  36855  2sb5nd  36897  dfvd1ir  36914  dfvd2anir  36925  dfvd2ir  36927  dfvd3ir  36934  dfvd3anir  36937  iden2  36964  e0bir  37137  uun2221p1  37174  uun2221p2  37175  2sb5ndVD  37280  2sb5ndALT  37302  iunconlem2  37305  fnchoice  37323  elini  37353  unisn0  37367  fsumiunss  37595  resincncf  37692  dvnprodlem3  37763  mbf0  37774  volioc  37789  stoweidlem13  37813  stoweidlem34  37835  stirlinglem5  37880  stirlinglem13  37888  stirlingr  37892  fourierdlem42  37952  fourierdlem42OLD  37953  fourierdlem62  37972  fouriersw  38035  etransc  38089  sge0rnn0  38118  gsumge0cl  38121  sge00  38126  sge0resplit  38156  omeiunle  38246  0ome  38258  volico  38267  icoresmbl  38269  ovn0lem  38291  ovnhoilem1  38327  aistia  38355  aisfina  38356  aiffnbandciffatnotciffb  38362  axorbciffatcxorb  38363  abnotbtaxb  38374  abnotataxb  38375  0noddALTV  38688  2noddALTV  38692  nnsum3primes4  38753  evengpop3  38763  pfx2  38823  uhgr0e  38994  uhgr0  38996  umgr0  39013  usgr0e  39093  usgr0  39099  usgrexmpllem  39109  usgrexmpl  39112  uvtxumgrres  39238  cplgr0  39250  usgrexi  39263  usgra2pthspth  39285  usgra2pthlem1  39287  uhg0e  39308  oddinmgm  39435  2zrngamgm  39559  2zrngaabl  39564  2zrngmmgm  39566  2zrngnring  39572  fldhmsubc  39706  fldhmsubcALTV  39725  eliunxp2  39737  zlmodzxzldeplem  39913  zlmodzxzldep  39919  ldepslinc  39924  3halfnz  39939  ex-gte  40071  empty-surprise  40143  eximp-surprise2  40146