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  698  stabnot  841  mpbir2an  951  mpbir3an  1206  tru  1402  dcfromnotnotr  1493  dcfromcon  1494  dcfrompeirce  1495  mpgbir  1502  nfxfr  1523  19.8a  1639  sbt  1833  dveeq2  1864  dveeq2or  1865  sbequilem  1887  cbvex2  1974  dvelimALT  2066  dvelimfv  2067  dvelimor  2074  nfeuv  2100  moaneu  2159  moanmo  2160  eqeltri  2307  nfcxfr  2383  neir  2417  neirr  2423  eqnetri  2437  nesymir  2461  nelir  2512  mprgbir  2602  vex  2818  issetri  2825  moeq  2995  cdeqi  3030  ru  3044  eqsstri  3274  3sstr4i  3283  mosn  3730  rabrsndc  3764  tpid1  3808  tpid2  3810  tpid3  3813  pwv  3918  uni0  3946  eqbrtri  4135  tr0  4224  trv  4225  zfnuleu  4239  0ex  4242  inex1  4249  elpwi2  4275  0elpw  4282  axpow2  4294  axpow3  4295  vpwex  4297  zfpair2  4328  exss  4348  opwo0id  4370  moop2  4373  pwundifss  4411  po0  4437  epse  4468  fr0  4477  0elon  4518  onm  4527  uniex2  4562  snnex  4574  ordtriexmidlem  4646  ordtriexmid  4648  ontr2exmid  4652  ordtri2or2exmidlem  4653  onsucsssucexmid  4654  onsucelsucexmidlem  4656  ruALT  4678  zfregfr  4701  dcextest  4708  zfinf2  4716  omex  4720  finds  4727  finds2  4728  ordom  4734  omsinds  4749  relsnop  4861  relxp  4864  rel0  4882  relopabiv  4883  relopabi  4885  eliunxp  4899  opeliunxp2  4900  dmi  4976  xpidtr  5158  cnvcnv  5220  dmsn0  5235  cnvsn0  5236  funmpt  5395  funmpt2  5396  funinsn  5410  isarep2  5448  f0  5563  f10  5654  f10d  5655  f1o00  5656  f1oi  5659  f1osn  5661  brprcneu  5668  fvopab3ig  5756  opabex  5915  eufnfv  5922  rinvf1o  6008  mpofun  6163  reldmmpo  6173  ovid  6178  ovidig  6179  ovidi  6180  ovig  6183  ovi3  6199  relmptopab  6264  oprabex  6334  oprabex3  6335  f1stres  6366  f2ndres  6367  opeliunxp2f  6482  tpos0  6518  issmo  6532  tfrlem6  6560  tfrlem8  6562  tfri1dALT  6595  tfrcl  6608  rdgfun  6617  frecfun  6639  frecfcllem  6648  0lt1o  6686  eqer  6812  ecopover  6880  ecopoverg  6883  th3qcor  6886  mapsnf1o3  6945  ssdomg  7031  ensn1  7049  xpcomf1o  7089  fiunsnnn  7151  finexdc  7173  elssdc  7175  exmidpw  7181  fissfi  7229  dcfi  7281  omct  7421  infnninf  7428  infnninfOLD  7429  pm54.43  7500  exmidonfinlem  7509  pw1on  7549  pw1dom2  7550  pw1ne1  7552  2oneel  7586  dmaddpi  7656  dmmulpi  7657  1lt2pi  7671  indpi  7673  1lt2nq  7737  genpelxp  7842  ltexprlempr  7939  recexprlempr  7963  cauappcvgprlemcl  7984  cauappcvgprlemladd  7989  caucvgprlemcl  8007  caucvgprprlemcl  8035  m1p1sr  8091  m1m1sr  8092  0lt1sr  8096  peano1nnnn  8183  ax1cn  8192  ax1re  8193  axaddf  8199  axmulf  8200  ax0lt1  8207  0lt1  8416  subaddrii  8578  ixi  8874  1ap0  8881  sup3exmid  9248  nn1suc  9273  neg1lt0  9362  4d2e2  9415  iap0  9478  un0mulcl  9547  pnf0xnn0  9587  3halfnz  9693  nummac  9771  uzf  9874  mnfltpnf  10137  ixxf  10250  ioof  10323  fzf  10365  fzp1disj  10436  fzp1nel  10460  fzo0  10526  frecfzennn  10812  frechashgf1o  10814  xnn0nnen  10823  fxnn0nninf  10825  seq3f1olemp  10901  sq0  11016  irec  11025  hash0  11184  prhash2ex  11199  hashfibclem  11231  climmo  12008  sum0  12099  fisumcom2  12149  prod0  12296  fprodcom2fi  12337  cos1bnd  12470  cos2bnd  12471  3dvds  12575  n2dvdsm1  12624  n2dvds3  12626  flodddiv4  12647  3lcm2e6woprm  12808  6lcm4e12  12809  2prm  12849  3lcm2e6  12882  pockthi  13081  modsubi  13142  ballotfilemcdc  13167  ballotfilem2  13172  ballotfilemic  13194  ballotfilem7  13223  ballotfilemth  13225  unennn  13232  ssnnctlemct  13281  structcnvcnv  13312  strleun  13401  starvndxnbasendx  13439  starvndxnplusgndx  13440  starvndxnmulrndx  13441  scandxnbasendx  13451  scandxnplusgndx  13452  scandxnmulrndx  13453  vscandxnbasendx  13456  vscandxnplusgndx  13457  vscandxnmulrndx  13458  vscandxnscandx  13459  ipndxnbasendx  13469  ipndxnplusgndx  13470  ipndxnmulrndx  13471  slotsdifipndx  13472  tsetndxnplusgndx  13489  tsetndxnmulrndx  13490  tsetndxnstarvndx  13491  slotstnscsi  13492  plendxnplusgndx  13503  plendxnmulrndx  13504  plendxnscandx  13505  plendxnvscandx  13506  slotsdifplendx  13507  basendxnocndx  13510  plendxnocndx  13511  dsndxnplusgndx  13518  dsndxnmulrndx  13519  slotsdnscsi  13520  dsndxntsetndx  13521  slotsdifdsndx  13522  unifndxntsetndx  13528  slotsdifunifndx  13529  restid  13547  mgmidmo  13635  gfsum0  14104  prdsval  14115  opprringb  14324  reldvdsr  14336  rrgmex  14507  lssmex  14629  lidlmex  14749  2idlmex  14775  fczpsrbag  14946  tgdom  15063  tgidm  15065  resttopon  15162  rest0  15170  psmetrel  15313  metrel  15333  xmetrel  15334  xmetf  15341  0met  15375  mopnrel  15432  setsmsbasg  15470  setsmsdsg  15471  qtopbasss  15512  reldvg  15670  dvexp  15702  dveflem  15717  elply2  15726  elplyd  15732  ply1term  15734  plymullem  15741  efcn  15759  sinhalfpilem  15782  sincosq1lem  15816  tangtx  15829  sincos4thpi  15831  pigt3  15835  dfrelog  15851  relogf1o  15852  log1  15857  loge  15858  relogiso  15864  2logb9irr  15962  2logb9irrap  15968  2sqlem9  16123  2sqlem10  16124  uhgr0e  16203  uhgr0  16206  umgrbien  16231  usgr0  16360  griedg0prc  16371  1loopgruspgr  16424  konigsbergumgr  16608  konigsberglem1  16609  ex-fl  16619  bj-nndcALT  16656  bj-axempty  16789  bj-axempty2  16790  bdinex1  16795  bj-zfpair2  16806  bj-uniex2  16812  bj-indint  16827  bj-omind  16830  bj-omex  16838  bj-omelon  16857  pw1ndom3  16890  0nninf  16908  dceqnconst  16972  dcapnconst  16973