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  686  stabnot  828  mpbir2an  937  mpbir3an  1174  tru  1352  mpgbir  1446  nfxfr  1467  19.8a  1583  sbt  1777  dveeq2  1808  dveeq2or  1809  sbequilem  1831  cbvex2  1915  dvelimALT  2003  dvelimfv  2004  dvelimor  2011  nfeuv  2037  moaneu  2095  moanmo  2096  eqeltri  2243  nfcxfr  2309  neir  2343  neirr  2349  eqnetri  2363  nesymir  2387  nelir  2438  mprgbir  2528  vex  2733  issetri  2739  moeq  2905  cdeqi  2940  ru  2954  eqsstri  3179  3sstr4i  3188  rgenm  3517  mosn  3619  rabrsndc  3651  tpid1  3694  tpid2  3696  tpid3  3699  pwv  3795  uni0  3823  eqbrtri  4010  tr0  4098  trv  4099  zfnuleu  4113  0ex  4116  inex1  4123  elpwi2  4144  0elpw  4150  axpow2  4162  axpow3  4163  vpwex  4165  zfpair2  4195  exss  4212  moop2  4236  pwundifss  4270  po0  4296  epse  4327  fr0  4336  0elon  4377  onm  4386  uniex2  4421  snnex  4433  ordtriexmidlem  4503  ordtriexmid  4505  ontr2exmid  4509  ordtri2or2exmidlem  4510  onsucsssucexmid  4511  onsucelsucexmidlem  4513  ruALT  4535  zfregfr  4558  dcextest  4565  zfinf2  4573  omex  4577  finds  4584  finds2  4585  ordom  4591  omsinds  4606  relsnop  4717  relxp  4720  rel0  4736  relopabi  4737  eliunxp  4750  opeliunxp2  4751  dmi  4826  xpidtr  5001  cnvcnv  5063  dmsn0  5078  cnvsn0  5079  funmpt  5236  funmpt2  5237  funinsn  5247  isarep2  5285  f0  5388  f10  5476  f1o00  5477  f1oi  5480  f1osn  5482  brprcneu  5489  fvopab3ig  5570  opabex  5720  eufnfv  5726  mpofun  5955  reldmmpo  5964  ovid  5969  ovidig  5970  ovidi  5971  ovig  5974  ovi3  5989  oprabex  6107  oprabex3  6108  f1stres  6138  f2ndres  6139  opeliunxp2f  6217  tpos0  6253  issmo  6267  tfrlem6  6295  tfrlem8  6297  tfri1dALT  6330  tfrcl  6343  rdgfun  6352  frecfun  6374  frecfcllem  6383  0lt1o  6419  eqer  6545  ecopover  6611  ecopoverg  6614  th3qcor  6617  mapsnf1o3  6675  ssdomg  6756  ensn1  6774  xpcomf1o  6803  fiunsnnn  6859  finexdc  6880  exmidpw  6886  dcfi  6958  omct  7094  infnninf  7100  infnninfOLD  7101  pm54.43  7167  exmidonfinlem  7170  pw1on  7203  pw1dom2  7204  pw1ne1  7206  dmaddpi  7287  dmmulpi  7288  1lt2pi  7302  indpi  7304  1lt2nq  7368  genpelxp  7473  ltexprlempr  7570  recexprlempr  7594  cauappcvgprlemcl  7615  cauappcvgprlemladd  7620  caucvgprlemcl  7638  caucvgprprlemcl  7666  m1p1sr  7722  m1m1sr  7723  0lt1sr  7727  peano1nnnn  7814  ax1cn  7823  ax1re  7824  axaddf  7830  axmulf  7831  ax0lt1  7838  0lt1  8046  subaddrii  8208  ixi  8502  1ap0  8509  sup3exmid  8873  nn1suc  8897  neg1lt0  8986  4d2e2  9038  iap0  9101  un0mulcl  9169  pnf0xnn0  9205  3halfnz  9309  nummac  9387  uzf  9490  mnfltpnf  9742  ixxf  9855  ioof  9928  fzf  9969  fzp1disj  10036  fzp1nel  10060  fzo0  10124  frecfzennn  10382  frechashgf1o  10384  fxnn0nninf  10394  seq3f1olemp  10458  sq0  10566  irec  10575  hash0  10731  prhash2ex  10744  climmo  11261  sum0  11351  fisumcom2  11401  prod0  11548  fprodcom2fi  11589  cos1bnd  11722  cos2bnd  11723  n2dvdsm1  11872  n2dvds3  11874  flodddiv4  11893  3lcm2e6woprm  12040  6lcm4e12  12041  2prm  12081  3lcm2e6  12114  pockthi  12310  unennn  12352  ssnnctlemct  12401  structcnvcnv  12432  strleun  12507  restid  12590  mgmidmo  12626  tgdom  12866  tgidm  12868  resttopon  12965  rest0  12973  psmetrel  13116  metrel  13136  xmetrel  13137  xmetf  13144  0met  13178  mopnrel  13235  setsmsbasg  13273  setsmsdsg  13274  qtopbasss  13315  reldvg  13442  dvexp  13469  dveflem  13481  efcn  13483  sinhalfpilem  13506  sincosq1lem  13540  tangtx  13553  sincos4thpi  13555  pigt3  13559  dfrelog  13575  relogf1o  13576  log1  13581  loge  13582  relogiso  13588  2logb9irr  13683  2logb9irrap  13689  2sqlem9  13754  2sqlem10  13755  ex-fl  13760  bj-nndcALT  13793  bj-axempty  13928  bj-axempty2  13929  bdinex1  13934  bj-zfpair2  13945  bj-uniex2  13951  bj-indint  13966  bj-omind  13969  bj-omex  13977  bj-omelon  13996  0nninf  14037  dceqnconst  14091  dcapnconst  14092