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  1501  nic-mpALT  1551  nic-ax  1552  nic-axALT  1553  mpgbir  1669  nfxfr  1692  19.35ri  1737  ax5e  1753  ax6ev  1799  exan  2030  ax13  2103  euequ1  2272  moanmo  2331  axi12  2405  axext2  2408  eqeltri  2513  nfcxfr  2589  neir  2630  neirr  2635  exmidneOLD  2637  nesymirOLD  2707  eqnetri  2727  nelir  2768  mprgbir  2796  vex  3090  issetri  3094  moeq  3253  cdeqi  3290  eqsstri  3500  3sstr4i  3509  rabrsn  4073  tpid1  4116  tpid2  4117  tpid3  4119  pwv  4221  uni0  4249  eqbrtri  4445  tr0  4531  trv  4532  zfrep4  4546  zfnuleu  4553  axnulALT  4554  0ex  4557  inex1  4566  0elpw  4594  axpow2  4605  axpow3  4606  pwex  4608  dvdemo1  4657  zfpair2  4662  exss  4685  moop2  4716  pwundif  4761  po0  4790  epse  4837  relsnop  4959  relxp  4962  rel0  4978  relopabi  4979  eliunxp  4992  opeliunxp2  4993  dmi  5069  xpidtr  5242  xpima  5299  cnvcnv  5308  dmsn0  5323  cnvsn0  5324  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  tpos0  7011  wfrrel  7049  wfrlem14  7057  wfrlem16  7059  issmo  7075  tfrlem6  7108  tfrlem8  7110  tfrlem16  7119  tfr1a  7120  tfr1  7123  tz7.44lem1  7131  seqomlem2  7176  seqomlem3  7177  seqomlem4  7178  fnseqom  7180  0lt1o  7214  0we1  7216  eqer  7404  ecopover  7475  mapsnf1o3  7528  ssdomg  7622  ensn1  7640  snfi  7657  xpcomf1o  7667  map2xp  7748  limensuci  7754  sdom1  7778  unblem4  7832  fidomdm  7859  marypha1lem  7953  hartogslem1  8057  hartogs  8059  card2on  8069  ruALT  8116  inf2  8128  inf3lem6  8138  infeq5i  8141  zfinf2  8147  cantnflt  8176  cnfcom  8204  trcl  8211  tz9.1c  8213  tc2  8225  r1funlim  8236  r1fnon  8237  karden  8365  tskwe  8383  cardprclem  8412  pm54.43  8433  r0weon  8442  iunmapdisj  8452  alephfnon  8494  alephfplem4  8536  alephfp  8537  alephval3  8539  aceq3lem  8549  kmlem2  8579  cda1dif  8604  ackbij1  8666  ackbij2lem2  8668  ackbij2  8671  infpssrlem3  8733  hsmexlem4  8857  hsmexlem5  8858  axdc3lem4  8881  ac2  8889  axac3  8892  ac6  8908  axdclem2  8948  ondomon  8986  alephsucpw  8993  pwcfsdom  9006  cfpwsdom  9007  smobeth  9009  axpowndlem3  9022  zfcndun  9039  zfcndpow  9040  zfcndinf  9042  zfcndac  9043  wunex2  9162  uniwun  9164  wuncval2  9171  grur1  9244  axgroth5  9248  axgroth2  9249  axgroth6  9252  axgroth3  9255  grothtsk  9259  inaprc  9260  ltsopi  9312  dmaddpi  9314  dmmulpi  9315  1lt2pi  9329  nqerf  9354  addnqf  9372  mulnqf  9373  1lt2nq  9397  m1p1sr  9515  m1m1sr  9516  0lt1sr  9518  axaddf  9568  axmulf  9569  ax1cn  9572  subaddrii  9963  ixi  10240  recgt0ii  10512  nn1suc  10630  neg1lt0  10716  4d2e2  10766  arch  10866  un0mulcl  10904  nummac  11083  uzf  11162  indstr  11227  mnfltpnf  11428  ixxf  11645  ioof  11732  fzf  11786  0nelfz1  11816  fzp1disj  11852  fzp1nel  11876  fzof  11915  om2uzrani  12163  om2uzf1oi  12164  uzrdglem  12168  uzrdgfni  12169  uzrdg0i  12170  ltwenn  12173  hashgf1o  12181  axdc4uzlem  12192  sq0  12363  irec  12371  facmapnn  12467  hashkf  12514  hashf  12519  hash0  12545  prhash2ex  12573  hashsslei  12593  hashxplem  12600  hashbclem  12610  hashf1lem1  12613  wrdexg  12669  wrd0OLD  12679  revs1  12855  0csh0  12880  cshw1  12906  cats1fvn  12939  relexp0g  13064  relexpsucnnr  13067  dfrtrclrec2  13099  rtrclreclem1  13100  rtrclreclem2  13101  rtrclreclem4  13103  dfrtrcl2  13104  climmo  13599  fsumcom2  13813  ackbijnn  13864  incexclem  13872  infcvgaux1i  13893  fprodcom2  14016  fprodn0f  14023  fprodge0  14025  fprodge1  14027  bpolylem  14079  bpoly3  14089  bpoly4  14090  efcvgfsum  14118  cos1bnd  14219  cos2bnd  14220  znnen  14243  qnnen  14244  aleph1re  14275  3dvds  14347  divalglem5  14353  bitsf  14375  sadcaddlem  14405  sadadd2lem  14407  sadadd3  14409  sadaddlem  14414  lcmf0  14578  lcmfunsnlem2lem1  14582  lcmfunsnlem2  14584  2prm  14611  coprmprod  14649  coprmproddvdslem  14650  3lcm2e6  14652  phicl2  14685  pockthi  14814  unbenlem  14815  prmrec  14829  vdwlem13  14906  vdwnn  14911  ramcl2  14936  ramcl2OLD  14937  lcmsmapnnOLD  14974  prmormapnnOLD  14977  prmgapprmo  14996  mod2xnegi  15006  modsubi  15007  prmo4  15062  prmo5  15063  prmo6  15064  structcnvcnv  15095  structfun  15096  setsres  15114  strfv  15120  strlemor1  15179  strleun  15182  0rest  15287  firest  15290  restid  15291  prdsval  15312  prdsbas  15314  prdsplusg  15315  prdsmulr  15316  prdsvsca  15317  prdsds  15321  imasaddfnlem  15385  imasvscafn  15394  oppchomfval  15570  oppcbas  15574  2oppchomf  15580  rescbas  15685  rescco  15688  rescabs  15689  0ssc  15693  0subcat  15694  idfucl  15737  wunnat  15812  homarel  15882  dmaf  15895  cdaf  15896  catcfuccl  15955  relxpchom  16017  catcxpccl  16043  oppchofcl  16096  oyoncl  16106  odubas  16330  letsr  16424  mgmidmo  16453  releqg  16815  ga0  16903  oppglem  16952  psgnunilem3  17088  psgnunilem4  17089  pmtrsn  17111  efgval  17302  efger  17303  efgsp1  17322  efgsfo  17324  efgredleme  17328  efgredlem  17332  efgred  17333  cygctb  17461  gsum2d2lem  17540  gsum2d2  17541  gsumcom2  17542  dprd2d2  17612  pgpfaclem1  17649  mgplem  17663  mgpress  17669  opprlem  17791  reldvdsr  17807  00lsp  18139  sralem  18335  srasca  18339  sravsca  18340  psrvscafval  18549  opsrbaslem  18636  psrbag0  18652  00ply1bas  18768  ply1plusgfvi  18770  xrsmgm  18938  zlmsca  19023  znbaslem  19040  resubdrg  19107  ocvfval  19160  ocv0  19171  cssval  19176  thlbas  19190  thlle  19191  islinds2  19302  matsca  19371  m2detleib  19587  tgdom  19925  tgidm  19927  indistps2ALT  19960  restbas  20105  resttopon  20108  rest0  20116  leordtval2  20159  iocpnfordt  20162  icomnfordt  20163  iooordt  20164  cnpfval  20181  iscnp2  20186  ist1-3  20296  1stcfb  20391  islly2  20430  comppfsc  20478  1stckgen  20500  ptbasfi  20527  xkotf  20531  dfac14  20564  opnfbas  20788  hauspwpwf1  20933  alexsubALTlem4  20996  alexsubALT  20997  ptcmplem5  21002  cnextrel  21009  ust0  21165  tuslem  21213  0met  21312  prdsdsf  21313  prdsxmetlem  21314  prdsmet  21316  setsmsbas  21421  setsmsds  21422  prdsbl  21437  tngds  21587  qtopbaslem  21690  xrtgioo  21735  xrsdsre  21739  zcld  21742  recld2  21743  sszcld  21746  reperflem  21747  retopcon  21758  iccpnfcnv  21868  bndth  21882  ishtpy  21896  nmoleub2lem2  22023  recmet  22184  resscdrg  22218  ishl2  22230  recms  22232  volf  22360  iundisj2  22379  volsup  22386  icombl  22394  ioombl  22395  ismbf3d  22487  0plef  22507  0pledm  22508  itg1ge0  22521  mbfi1fseqlem5  22554  itg2addlem  22593  iblcnlem1  22622  reldv  22702  limciun  22726  dvexp  22784  dveflem  22808  lhop1lem  22842  lhop  22845  elply2  23018  elplyd  23024  ply1term  23026  ply0  23030  plymullem  23038  qaa  23144  pserulm  23242  pserdvlem2  23248  efcn  23263  sincosq1lem  23317  tangtx  23325  sincos4thpi  23333  sincos6thpi  23335  pige3  23337  efif1olem4  23359  logf1o  23379  relogf1o  23381  log1  23400  loge  23401  relogiso  23412  dvrelog  23447  relogcn  23448  logcn  23457  cxpcn3  23553  resqrtcn  23554  leibpi  23733  log2ublem1  23737  birthday  23745  emcllem5  23790  harmonicbnd  23794  harmonicbnd2  23795  emgt0  23797  harmonicbnd3  23798  lgamgulm2  23826  lgamcvglem  23830  gamf  23833  ppiltx  23967  ppiublem1  23993  ppiub  23995  bclbnd  24071  bpos1lem  24073  bposlem8  24082  lgsquadlem2  24146  2sqlem9  24164  2sqlem10  24165  chebbnd1  24173  selberg2lem  24251  pntrsumo1  24266  selbergsb  24276  pntpbnd  24289  istrkg2ld  24371  ttgval  24751  ttglem  24752  cchhllem  24763  ax5seglem7  24811  axlowdimlem4  24821  axlowdimlem6  24823  axlowdimlem7  24824  axlowdimlem10  24827  axlowdimlem13  24830  axlowdimlem16  24833  uhgra0  24882  umgra0  24898  usgra0  24943  usgra1v  24963  cusgraexilem2  25040  cusgrasizeindslem2  25047  0wlk  25120  0trl  25121  wlkntrllem2  25135  wlkntrl  25137  0pth  25145  1pthonlem1  25164  usgrcyclnl2  25214  4cycl4dv  25240  wwlknext  25297  wwlknfi  25311  disjxwwlkn  25318  vdgrf  25471  umgrabi  25556  vdegp1ai  25557  vdegp1bi  25558  konigsberg  25560  frgra0  25567  numclwwlkdisj  25653  numclwwlk3lem  25681  ex-dif  25718  ex-in  25720  ex-eprel  25728  ex-id  25729  ex-fl  25742  avril1  25745  2bornot2b  25746  grposn  25788  issubgoi  25883  0vfval  26070  vsfval  26099  ajmoi  26345  ajfuni  26346  normlem2  26599  norm3adifii  26636  hhip  26665  hlim0  26723  hlimcaui  26724  hlimf  26725  hhssnv  26750  shscli  26805  shsval2i  26875  h1de2i  27041  fh3i  27111  fh4i  27112  cm2mi  27114  qlaxr3i  27124  mayetes3i  27217  ho0f  27239  hoif  27242  hodidi  27275  ho0subi  27283  hosd1i  27310  adjmo  27320  nmopsetn0  27353  nmfnsetn0  27366  funadj  27374  funcnvadj  27381  nmcexi  27514  cnlnadjlem8  27562  nmoptri2i  27587  opsqrlem4  27631  hmopidmchi  27639  pjoci  27668  pjinvari  27679  abrexdomjm  27977  elim2ifim  28001  iundisj2f  28039  mptexgf  28065  rinvf1o  28070  funcnvmptOLD  28110  dfcnv2  28119  snct  28138  dmct  28141  fpwrelmap  28161  iundisj2fi  28209  gsumle  28380  xrge0slmod  28446  xrge0pluscn  28585  zlmds  28607  zlmtset  28608  qqhre  28663  esumrnmpt2  28728  esumfsup  28730  esumpcvgval  28738  hasheuni  28745  esumcvg  28746  esumcvgsum  28748  esumsup  28749  esum2d  28753  dmsigagen  28805  ldgenpisyslem3  28826  measvuni  28875  voliune  28891  volfiniune  28892  br2base  28930  dya2iocuni  28944  eulerpartlem1  29026  eulerpartlemt  29030  eulerpartgbij  29031  fib0  29058  coinfliprv  29141  ballotlem2  29147  ballotlemic  29165  ballotlem7  29194  ballotth  29196  plymul02  29223  bnj226  29330  bnj1101  29384  bnj110  29457  bnj149  29474  bnj150  29475  bnj151  29476  bnj517  29484  bnj580  29512  bnj865  29522  bnj900  29528  bnj996  29554  bnj1110  29579  bnj1133  29586  bnj1128  29587  bnj1145  29590  bnj1137  29592  bnj1171  29597  bnj1176  29602  subfacp1lem5  29695  subfacp1lem6  29696  kur14lem9  29725  cvmcov2  29786  cvmliftlem1  29796  cvmliftlem4  29799  cvmliftlem5  29800  msrfo  29972  problem5  30089  ghomgrpilem2  30092  brtpid1  30141  brtpid2  30142  brtpid3  30143  logi  30157  faclimlem1  30166  domep  30226  axextndbi  30238  poseq  30278  frrlem10  30312  sltval2  30330  brv  30429  txprel  30431  relsset  30440  relbigcup  30449  fvbigcup  30454  fnsingle  30471  fvsingle  30472  snelsingles  30474  funimage  30480  fullfunfnv  30498  imagesset  30505  funtransport  30583  colinrel  30609  funray  30692  funline  30694  0hf  30729  neibastop2lem  30801  filnetlem3  30821  waj-ax  30859  lukshef-ax2  30860  arg-ax  30861  limsucncmpi  30890  bj-babylob  30971  bj-nalnalimiOLD  31002  bj-nfv  31006  bj-dvdemo1  31168  bj-disjcsn  31291  bj-snsetex  31306  bj-0eltag  31321  bj-2upln0  31366  bj-2upln1upl  31367  f1omptsnlem  31472  f1omptsn  31473  icoreresf  31489  relowlssretop  31500  relowlpssretop  31501  pigt3  31641  poimirlem3  31646  poimirlem9  31652  poimirlem16  31659  poimirlem17  31660  poimirlem18  31661  poimirlem19  31662  poimirlem20  31663  poimirlem26  31669  mblfinlem1  31680  mblfinlem2  31681  ismblfin  31684  voliunnfl  31687  cnambfre  31692  dvtanlemOLD  31694  cover2  31743  abrexdom  31760  fdc  31777  cncfres  31800  heibor1lem  31844  bicontr  32016  an12i  32037  tsim1  32075  ac6s6f  32119  elimhyps  32241  dedths  32242  renegclALT  32243  hlhilslem  35217  moxfr  35242  mapfzcons1  35267  diophrw  35309  0dioph  35329  vdioph  35330  rabren3dioph  35366  2nn0ind  35498  rpnnen3  35592  kelac2lem  35627  frlmpwfi  35661  ifpbiidcor2  35825  eliunov2  35909  xphe  36012  xpheOLD  36013  0he  36014  he0  36016  snhesn  36018  idhe  36019  frege54cor1c  36147  amgm2d  36286  amgm3d  36287  amgm4d  36288  lhe4.4ex1a  36314  rusbcALT  36426  ipo0  36438  ifr0  36439  vk15.4j  36521  2sb5nd  36563  dfvd1ir  36580  dfvd2anir  36591  dfvd2ir  36593  dfvd3ir  36600  dfvd3anir  36603  iden2  36630  e0bir  36803  uun2221p1  36840  uun2221p2  36841  2sb5ndVD  36946  2sb5ndALT  36968  iunconlem2  36971  fnchoice  36989  elini  37019  unisn0  37034  fsumiunss  37228  resincncf  37323  dvnprodlem3  37391  mbf0  37402  volioc  37417  stoweidlem13  37441  stoweidlem34  37463  stirlinglem5  37508  stirlinglem13  37516  stirlingr  37520  fourierdlem42  37579  fourierdlem62  37599  fouriersw  37662  etransc  37714  sge0rnn0  37743  gsumge0cl  37746  sge00  37751  sge0resplit  37781  omeiunle  37846  aistia  37883  aisfina  37884  aiffnbandciffatnotciffb  37890  axorbciffatcxorb  37891  abnotbtaxb  37902  abnotataxb  37903  0noddALTV  38207  2noddALTV  38211  nnsum3primes4  38272  evengpop3  38282  pfx2  38342  usgra2pthspth  38420  usgra2pthlem1  38422  uhg0e  38445  oddinmgm  38572  2zrngamgm  38696  2zrngaabl  38701  2zrngmmgm  38703  2zrngnring  38709  fldhmsubc  38843  fldhmsubcALTV  38862  eliunxp2  38874  zlmodzxzldeplem  39050  zlmodzxzldep  39056  ldepslinc  39061  3halfnz  39077  ex-gte  39209  empty-surprise  39281  eximp-surprise2  39284