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  681  stabnot  819  mpbir2an  927  mpbir3an  1164  tru  1339  mpgbir  1433  nfxfr  1454  19.8a  1570  sbt  1764  dveeq2  1795  dveeq2or  1796  sbequilem  1818  cbvex2  1902  dvelimALT  1990  dvelimfv  1991  dvelimor  1998  nfeuv  2024  moaneu  2082  moanmo  2083  eqeltri  2230  nfcxfr  2296  neir  2330  neirr  2336  eqnetri  2350  nesymir  2374  nelir  2425  mprgbir  2515  vex  2715  issetri  2721  moeq  2887  cdeqi  2922  ru  2936  eqsstri  3160  3sstr4i  3169  rgenm  3496  mosn  3595  rabrsndc  3627  tpid1  3670  tpid2  3672  tpid3  3675  pwv  3771  uni0  3799  eqbrtri  3985  tr0  4073  trv  4074  zfnuleu  4088  0ex  4091  inex1  4098  elpwi2  4119  0elpw  4125  axpow2  4137  axpow3  4138  vpwex  4140  zfpair2  4170  exss  4187  moop2  4211  pwundifss  4245  po0  4271  epse  4302  fr0  4311  0elon  4352  onm  4361  uniex2  4396  snnex  4408  ordtriexmidlem  4478  ordtriexmid  4480  ontr2exmid  4484  ordtri2or2exmidlem  4485  onsucsssucexmid  4486  onsucelsucexmidlem  4488  ruALT  4510  zfregfr  4533  dcextest  4540  zfinf2  4548  omex  4552  finds  4559  finds2  4560  ordom  4566  omsinds  4581  relsnop  4692  relxp  4695  rel0  4711  relopabi  4712  eliunxp  4725  opeliunxp2  4726  dmi  4801  xpidtr  4976  cnvcnv  5038  dmsn0  5053  cnvsn0  5054  funmpt  5208  funmpt2  5209  funinsn  5219  isarep2  5257  f0  5360  f10  5448  f1o00  5449  f1oi  5452  f1osn  5454  brprcneu  5461  fvopab3ig  5542  opabex  5691  eufnfv  5697  mpofun  5923  reldmmpo  5932  ovid  5937  ovidig  5938  ovidi  5939  ovig  5942  ovi3  5957  oprabex  6076  oprabex3  6077  f1stres  6107  f2ndres  6108  opeliunxp2f  6185  tpos0  6221  issmo  6235  tfrlem6  6263  tfrlem8  6265  tfri1dALT  6298  tfrcl  6311  rdgfun  6320  frecfun  6342  frecfcllem  6351  0lt1o  6387  eqer  6512  ecopover  6578  ecopoverg  6581  th3qcor  6584  mapsnf1o3  6642  ssdomg  6723  ensn1  6741  xpcomf1o  6770  fiunsnnn  6826  finexdc  6847  exmidpw  6853  dcfi  6925  omct  7061  infnninf  7067  infnninfOLD  7068  pm54.43  7125  exmidonfinlem  7128  pw1on  7161  pw1dom2  7162  pw1ne1  7164  dmaddpi  7245  dmmulpi  7246  1lt2pi  7260  indpi  7262  1lt2nq  7326  genpelxp  7431  ltexprlempr  7528  recexprlempr  7552  cauappcvgprlemcl  7573  cauappcvgprlemladd  7578  caucvgprlemcl  7596  caucvgprprlemcl  7624  m1p1sr  7680  m1m1sr  7681  0lt1sr  7685  peano1nnnn  7772  ax1cn  7781  ax1re  7782  axaddf  7788  axmulf  7789  ax0lt1  7796  0lt1  8002  subaddrii  8164  ixi  8458  1ap0  8465  sup3exmid  8828  nn1suc  8852  neg1lt0  8941  4d2e2  8993  iap0  9056  un0mulcl  9124  pnf0xnn0  9160  3halfnz  9261  nummac  9339  uzf  9442  mnfltpnf  9692  ixxf  9802  ioof  9875  fzf  9916  fzp1disj  9982  fzp1nel  10006  fzo0  10067  frecfzennn  10325  frechashgf1o  10327  fxnn0nninf  10337  seq3f1olemp  10401  sq0  10509  irec  10518  hash0  10671  prhash2ex  10683  climmo  11195  sum0  11285  fisumcom2  11335  prod0  11482  fprodcom2fi  11523  cos1bnd  11656  cos2bnd  11657  n2dvdsm1  11804  n2dvds3  11806  flodddiv4  11825  3lcm2e6woprm  11963  6lcm4e12  11964  2prm  12004  3lcm2e6  12035  unennn  12137  ssnnctlemct  12186  structcnvcnv  12217  strleun  12290  restid  12373  tgdom  12483  tgidm  12485  resttopon  12582  rest0  12590  psmetrel  12733  metrel  12753  xmetrel  12754  xmetf  12761  0met  12795  mopnrel  12852  setsmsbasg  12890  setsmsdsg  12891  qtopbasss  12932  reldvg  13059  dvexp  13086  dveflem  13098  efcn  13100  sinhalfpilem  13123  sincosq1lem  13157  tangtx  13170  sincos4thpi  13172  pigt3  13176  dfrelog  13192  relogf1o  13193  log1  13198  loge  13199  relogiso  13205  2logb9irr  13299  2logb9irrap  13305  ex-fl  13312  bj-nndcALT  13341  bj-axempty  13479  bj-axempty2  13480  bdinex1  13485  bj-zfpair2  13496  bj-uniex2  13502  bj-indint  13517  bj-omind  13520  bj-omex  13528  bj-omelon  13547  0nninf  13587  dceqnconst  13641  dcapnconst  13642