Theorem mpbir 145

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

Syntax hints:   <-> wb 104

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

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  pm5.74ri  180  imnani  680  stabnot  818  mpbir2an  926  mpbir3an  1163  tru  1335  mpgbir  1429  nfxfr  1450  19.8a  1569  sbt  1757  dveeq2  1787  dveeq2or  1788  sbequilem  1810  cbvex2  1894  dvelimALT  1985  dvelimfv  1986  dvelimor  1993  nfeuv  2017  moaneu  2075  moanmo  2076  eqeltri  2212  nfcxfr  2278  neir  2311  neirr  2317  eqnetri  2331  nesymir  2355  nelir  2406  mprgbir  2490  vex  2689  issetri  2695  moeq  2859  cdeqi  2894  ru  2908  eqsstri  3129  3sstr4i  3138  rgenm  3465  mosn  3560  rabrsndc  3591  tpid1  3634  tpid2  3636  tpid3  3639  pwv  3735  uni0  3763  eqbrtri  3949  tr0  4037  trv  4038  zfnuleu  4052  0ex  4055  inex1  4062  0elpw  4088  axpow2  4100  axpow3  4101  vpwex  4103  zfpair2  4132  exss  4149  moop2  4173  pwundifss  4207  po0  4233  epse  4264  fr0  4273  0elon  4314  onm  4323  uniex2  4358  snnex  4369  ordtriexmidlem  4435  ordtriexmid  4437  ontr2exmid  4440  ordtri2or2exmidlem  4441  onsucsssucexmid  4442  onsucelsucexmidlem  4444  ruALT  4466  zfregfr  4488  dcextest  4495  zfinf2  4503  omex  4507  finds  4514  finds2  4515  ordom  4520  omsinds  4535  relsnop  4645  relxp  4648  rel0  4664  relopabi  4665  eliunxp  4678  opeliunxp2  4679  dmi  4754  xpidtr  4929  cnvcnv  4991  dmsn0  5006  cnvsn0  5007  funmpt  5161  funmpt2  5162  funinsn  5172  isarep2  5210  f0  5313  f10  5401  f1o00  5402  f1oi  5405  f1osn  5407  brprcneu  5414  fvopab3ig  5495  opabex  5644  eufnfv  5648  mpofun  5873  reldmmpo  5882  ovid  5887  ovidig  5888  ovidi  5889  ovig  5892  ovi3  5907  oprabex  6026  oprabex3  6027  f1stres  6057  f2ndres  6058  opeliunxp2f  6135  tpos0  6171  issmo  6185  tfrlem6  6213  tfrlem8  6215  tfri1dALT  6248  tfrcl  6261  rdgfun  6270  frecfun  6292  frecfcllem  6301  0lt1o  6337  eqer  6461  ecopover  6527  ecopoverg  6530  th3qcor  6533  mapsnf1o3  6591  ssdomg  6672  ensn1  6690  xpcomf1o  6719  fiunsnnn  6775  finexdc  6796  exmidpw  6802  omct  7002  infnninf  7022  nnnninf  7023  pm54.43  7046  exmidonfinlem  7049  dmaddpi  7133  dmmulpi  7134  1lt2pi  7148  indpi  7150  1lt2nq  7214  genpelxp  7319  ltexprlempr  7416  recexprlempr  7440  cauappcvgprlemcl  7461  cauappcvgprlemladd  7466  caucvgprlemcl  7484  caucvgprprlemcl  7512  m1p1sr  7568  m1m1sr  7569  0lt1sr  7573  peano1nnnn  7660  ax1cn  7669  ax1re  7670  axaddf  7676  axmulf  7677  ax0lt1  7684  0lt1  7889  subaddrii  8051  ixi  8345  1ap0  8352  sup3exmid  8715  nn1suc  8739  neg1lt0  8828  4d2e2  8880  iap0  8943  un0mulcl  9011  pnf0xnn0  9047  3halfnz  9148  nummac  9226  uzf  9329  mnfltpnf  9571  ixxf  9681  ioof  9754  fzf  9794  fzp1disj  9860  fzp1nel  9884  fzo0  9945  frecfzennn  10199  frechashgf1o  10201  fxnn0nninf  10211  seq3f1olemp  10275  sq0  10383  irec  10392  hash0  10543  prhash2ex  10555  climmo  11067  sum0  11157  fisumcom2  11207  cos1bnd  11466  cos2bnd  11467  n2dvdsm1  11610  n2dvds3  11612  flodddiv4  11631  3lcm2e6woprm  11767  6lcm4e12  11768  2prm  11808  3lcm2e6  11838  unennn  11910  structcnvcnv  11975  strleun  12048  restid  12131  tgdom  12241  tgidm  12243  resttopon  12340  rest0  12348  psmetrel  12491  metrel  12511  xmetrel  12512  xmetf  12519  0met  12553  mopnrel  12610  setsmsbasg  12648  setsmsdsg  12649  qtopbasss  12690  reldvg  12817  dvexp  12844  dveflem  12855  efcn  12857  sinhalfpilem  12872  sincosq1lem  12906  tangtx  12919  sincos4thpi  12921  pigt3  12925  ex-fl  12937  bj-nndcALT  12963  bj-axempty  13091  bj-axempty2  13092  bdinex1  13097  bj-zfpair2  13108  bj-uniex2  13114  bj-indint  13129  bj-omind  13132  bj-omex  13140  bj-omelon  13159  pw1dom2  13190  0nninf  13197