Theorem mpbir 146

Description: An inference from a biconditional, related to modus ponens. (Contributed by NM, 5-Aug-1993.)

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

Syntax hints:   <-> wb 105

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  pm5.74ri  181  imnani  691  stabnot  833  mpbir2an  942  mpbir3an  1179  tru  1357  mpgbir  1453  nfxfr  1474  19.8a  1590  sbt  1784  dveeq2  1815  dveeq2or  1816  sbequilem  1838  cbvex2  1922  dvelimALT  2010  dvelimfv  2011  dvelimor  2018  nfeuv  2044  moaneu  2102  moanmo  2103  eqeltri  2250  nfcxfr  2316  neir  2350  neirr  2356  eqnetri  2370  nesymir  2394  nelir  2445  mprgbir  2535  vex  2741  issetri  2747  moeq  2913  cdeqi  2948  ru  2962  eqsstri  3188  3sstr4i  3197  rgenm  3526  mosn  3629  rabrsndc  3661  tpid1  3704  tpid2  3706  tpid3  3709  pwv  3809  uni0  3837  eqbrtri  4025  tr0  4113  trv  4114  zfnuleu  4128  0ex  4131  inex1  4138  elpwi2  4159  0elpw  4165  axpow2  4177  axpow3  4178  vpwex  4180  zfpair2  4211  exss  4228  moop2  4252  pwundifss  4286  po0  4312  epse  4343  fr0  4352  0elon  4393  onm  4402  uniex2  4437  snnex  4449  ordtriexmidlem  4519  ordtriexmid  4521  ontr2exmid  4525  ordtri2or2exmidlem  4526  onsucsssucexmid  4527  onsucelsucexmidlem  4529  ruALT  4551  zfregfr  4574  dcextest  4581  zfinf2  4589  omex  4593  finds  4600  finds2  4601  ordom  4607  omsinds  4622  relsnop  4733  relxp  4736  rel0  4752  relopabi  4753  eliunxp  4767  opeliunxp2  4768  dmi  4843  xpidtr  5020  cnvcnv  5082  dmsn0  5097  cnvsn0  5098  funmpt  5255  funmpt2  5256  funinsn  5266  isarep2  5304  f0  5407  f10  5496  f1o00  5497  f1oi  5500  f1osn  5502  brprcneu  5509  fvopab3ig  5591  opabex  5741  eufnfv  5748  mpofun  5977  reldmmpo  5986  ovid  5991  ovidig  5992  ovidi  5993  ovig  5996  ovi3  6011  oprabex  6129  oprabex3  6130  f1stres  6160  f2ndres  6161  opeliunxp2f  6239  tpos0  6275  issmo  6289  tfrlem6  6317  tfrlem8  6319  tfri1dALT  6352  tfrcl  6365  rdgfun  6374  frecfun  6396  frecfcllem  6405  0lt1o  6441  eqer  6567  ecopover  6633  ecopoverg  6636  th3qcor  6639  mapsnf1o3  6697  ssdomg  6778  ensn1  6796  xpcomf1o  6825  fiunsnnn  6881  finexdc  6902  exmidpw  6908  dcfi  6980  omct  7116  infnninf  7122  infnninfOLD  7123  pm54.43  7189  exmidonfinlem  7192  pw1on  7225  pw1dom2  7226  pw1ne1  7228  2oneel  7255  dmaddpi  7324  dmmulpi  7325  1lt2pi  7339  indpi  7341  1lt2nq  7405  genpelxp  7510  ltexprlempr  7607  recexprlempr  7631  cauappcvgprlemcl  7652  cauappcvgprlemladd  7657  caucvgprlemcl  7675  caucvgprprlemcl  7703  m1p1sr  7759  m1m1sr  7760  0lt1sr  7764  peano1nnnn  7851  ax1cn  7860  ax1re  7861  axaddf  7867  axmulf  7868  ax0lt1  7875  0lt1  8084  subaddrii  8246  ixi  8540  1ap0  8547  sup3exmid  8914  nn1suc  8938  neg1lt0  9027  4d2e2  9079  iap0  9142  un0mulcl  9210  pnf0xnn0  9246  3halfnz  9350  nummac  9428  uzf  9531  mnfltpnf  9785  ixxf  9898  ioof  9971  fzf  10012  fzp1disj  10080  fzp1nel  10104  fzo0  10168  frecfzennn  10426  frechashgf1o  10428  fxnn0nninf  10438  seq3f1olemp  10502  sq0  10611  irec  10620  hash0  10776  prhash2ex  10789  climmo  11306  sum0  11396  fisumcom2  11446  prod0  11593  fprodcom2fi  11634  cos1bnd  11767  cos2bnd  11768  n2dvdsm1  11918  n2dvds3  11920  flodddiv4  11939  3lcm2e6woprm  12086  6lcm4e12  12087  2prm  12127  3lcm2e6  12160  pockthi  12356  unennn  12398  ssnnctlemct  12447  structcnvcnv  12478  strleun  12563  starvndxnbasendx  12600  starvndxnplusgndx  12601  starvndxnmulrndx  12602  scandxnbasendx  12612  scandxnplusgndx  12613  scandxnmulrndx  12614  vscandxnbasendx  12617  vscandxnplusgndx  12618  vscandxnmulrndx  12619  vscandxnscandx  12620  ipndxnbasendx  12630  ipndxnplusgndx  12631  ipndxnmulrndx  12632  slotsdifipndx  12633  tsetndxnplusgndx  12647  tsetndxnmulrndx  12648  tsetndxnstarvndx  12649  slotstnscsi  12650  plendxnplusgndx  12661  plendxnmulrndx  12662  plendxnscandx  12663  plendxnvscandx  12664  slotsdifplendx  12665  dsndxnplusgndx  12672  dsndxnmulrndx  12673  slotsdnscsi  12674  dsndxntsetndx  12675  slotsdifdsndx  12676  unifndxntsetndx  12682  slotsdifunifndx  12683  restid  12699  mgmidmo  12791  tgdom  13575  tgidm  13577  resttopon  13674  rest0  13682  psmetrel  13825  metrel  13845  xmetrel  13846  xmetf  13853  0met  13887  mopnrel  13944  setsmsbasg  13982  setsmsdsg  13983  qtopbasss  14024  reldvg  14151  dvexp  14178  dveflem  14190  efcn  14192  sinhalfpilem  14215  sincosq1lem  14249  tangtx  14262  sincos4thpi  14264  pigt3  14268  dfrelog  14284  relogf1o  14285  log1  14290  loge  14291  relogiso  14297  2logb9irr  14392  2logb9irrap  14398  2sqlem9  14474  2sqlem10  14475  ex-fl  14480  bj-nndcALT  14513  bj-axempty  14648  bj-axempty2  14649  bdinex1  14654  bj-zfpair2  14665  bj-uniex2  14671  bj-indint  14686  bj-omind  14689  bj-omex  14697  bj-omelon  14716  0nninf  14756  dceqnconst  14810  dcapnconst  14811