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  692  stabnot  834  mpbir2an  944  mpbir3an  1181  tru  1376  dcfromnotnotr  1466  dcfromcon  1467  dcfrompeirce  1468  mpgbir  1475  nfxfr  1496  19.8a  1612  sbt  1806  dveeq2  1837  dveeq2or  1838  sbequilem  1860  cbvex2  1945  dvelimALT  2037  dvelimfv  2038  dvelimor  2045  nfeuv  2071  moaneu  2129  moanmo  2130  eqeltri  2277  nfcxfr  2344  neir  2378  neirr  2384  eqnetri  2398  nesymir  2422  nelir  2473  mprgbir  2563  vex  2774  issetri  2780  moeq  2947  cdeqi  2982  ru  2996  eqsstri  3224  3sstr4i  3233  mosn  3668  rabrsndc  3700  tpid1  3743  tpid2  3745  tpid3  3748  pwv  3848  uni0  3876  eqbrtri  4064  tr0  4152  trv  4153  zfnuleu  4167  0ex  4170  inex1  4177  elpwi2  4201  0elpw  4207  axpow2  4219  axpow3  4220  vpwex  4222  zfpair2  4253  exss  4270  opwo0id  4292  moop2  4295  pwundifss  4331  po0  4357  epse  4388  fr0  4397  0elon  4438  onm  4447  uniex2  4482  snnex  4494  ordtriexmidlem  4566  ordtriexmid  4568  ontr2exmid  4572  ordtri2or2exmidlem  4573  onsucsssucexmid  4574  onsucelsucexmidlem  4576  ruALT  4598  zfregfr  4621  dcextest  4628  zfinf2  4636  omex  4640  finds  4647  finds2  4648  ordom  4654  omsinds  4669  relsnop  4780  relxp  4783  rel0  4799  relopabiv  4800  relopabi  4802  eliunxp  4816  opeliunxp2  4817  dmi  4892  xpidtr  5072  cnvcnv  5134  dmsn0  5149  cnvsn0  5150  funmpt  5308  funmpt2  5309  funinsn  5322  isarep2  5360  f0  5465  f10  5555  f1o00  5556  f1oi  5559  f1osn  5561  brprcneu  5568  fvopab3ig  5652  opabex  5807  eufnfv  5814  mpofun  6046  reldmmpo  6056  ovid  6061  ovidig  6062  ovidi  6063  ovig  6066  ovi3  6082  oprabex  6212  oprabex3  6213  f1stres  6244  f2ndres  6245  opeliunxp2f  6323  tpos0  6359  issmo  6373  tfrlem6  6401  tfrlem8  6403  tfri1dALT  6436  tfrcl  6449  rdgfun  6458  frecfun  6480  frecfcllem  6489  0lt1o  6525  eqer  6651  ecopover  6719  ecopoverg  6722  th3qcor  6725  mapsnf1o3  6783  ssdomg  6869  ensn1  6887  xpcomf1o  6919  fiunsnnn  6977  finexdc  6998  exmidpw  7004  dcfi  7082  omct  7218  infnninf  7225  infnninfOLD  7226  pm54.43  7297  exmidonfinlem  7300  pw1on  7337  pw1dom2  7338  pw1ne1  7340  2oneel  7367  dmaddpi  7437  dmmulpi  7438  1lt2pi  7452  indpi  7454  1lt2nq  7518  genpelxp  7623  ltexprlempr  7720  recexprlempr  7744  cauappcvgprlemcl  7765  cauappcvgprlemladd  7770  caucvgprlemcl  7788  caucvgprprlemcl  7816  m1p1sr  7872  m1m1sr  7873  0lt1sr  7877  peano1nnnn  7964  ax1cn  7973  ax1re  7974  axaddf  7980  axmulf  7981  ax0lt1  7988  0lt1  8198  subaddrii  8360  ixi  8655  1ap0  8662  sup3exmid  9029  nn1suc  9054  neg1lt0  9143  4d2e2  9196  iap0  9259  un0mulcl  9328  pnf0xnn0  9364  3halfnz  9469  nummac  9547  uzf  9650  mnfltpnf  9906  ixxf  10019  ioof  10092  fzf  10133  fzp1disj  10201  fzp1nel  10225  fzo0  10290  frecfzennn  10569  frechashgf1o  10571  xnn0nnen  10580  fxnn0nninf  10582  seq3f1olemp  10658  sq0  10773  irec  10782  hash0  10939  prhash2ex  10952  climmo  11551  sum0  11641  fisumcom2  11691  prod0  11838  fprodcom2fi  11879  cos1bnd  12012  cos2bnd  12013  3dvds  12117  n2dvdsm1  12166  n2dvds3  12168  flodddiv4  12189  3lcm2e6woprm  12350  6lcm4e12  12351  2prm  12391  3lcm2e6  12424  pockthi  12623  modsubi  12684  unennn  12710  ssnnctlemct  12759  structcnvcnv  12790  strleun  12878  starvndxnbasendx  12916  starvndxnplusgndx  12917  starvndxnmulrndx  12918  scandxnbasendx  12928  scandxnplusgndx  12929  scandxnmulrndx  12930  vscandxnbasendx  12933  vscandxnplusgndx  12934  vscandxnmulrndx  12935  vscandxnscandx  12936  ipndxnbasendx  12946  ipndxnplusgndx  12947  ipndxnmulrndx  12948  slotsdifipndx  12949  tsetndxnplusgndx  12966  tsetndxnmulrndx  12967  tsetndxnstarvndx  12968  slotstnscsi  12969  plendxnplusgndx  12980  plendxnmulrndx  12981  plendxnscandx  12982  plendxnvscandx  12983  slotsdifplendx  12984  basendxnocndx  12987  plendxnocndx  12988  dsndxnplusgndx  12995  dsndxnmulrndx  12996  slotsdnscsi  12997  dsndxntsetndx  12998  slotsdifdsndx  12999  unifndxntsetndx  13005  slotsdifunifndx  13006  restid  13024  prdsval  13047  mgmidmo  13146  rrgmex  13965  lssmex  14059  lidlmex  14179  2idlmex  14205  fczpsrbag  14375  tgdom  14486  tgidm  14488  resttopon  14585  rest0  14593  psmetrel  14736  metrel  14756  xmetrel  14757  xmetf  14764  0met  14798  mopnrel  14855  setsmsbasg  14893  setsmsdsg  14894  qtopbasss  14935  reldvg  15093  dvexp  15125  dveflem  15140  elply2  15149  elplyd  15155  ply1term  15157  plymullem  15164  efcn  15182  sinhalfpilem  15205  sincosq1lem  15239  tangtx  15252  sincos4thpi  15254  pigt3  15258  dfrelog  15274  relogf1o  15275  log1  15280  loge  15281  relogiso  15287  2logb9irr  15385  2logb9irrap  15391  2sqlem9  15543  2sqlem10  15544  ex-fl  15594  bj-nndcALT  15627  bj-axempty  15762  bj-axempty2  15763  bdinex1  15768  bj-zfpair2  15779  bj-uniex2  15785  bj-indint  15800  bj-omind  15803  bj-omex  15811  bj-omelon  15830  0nninf  15874  dceqnconst  15932  dcapnconst  15933