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  1368  dcfromnotnotr  1458  dcfromcon  1459  dcfrompeirce  1460  mpgbir  1467  nfxfr  1488  19.8a  1604  sbt  1798  dveeq2  1829  dveeq2or  1830  sbequilem  1852  cbvex2  1937  dvelimALT  2029  dvelimfv  2030  dvelimor  2037  nfeuv  2063  moaneu  2121  moanmo  2122  eqeltri  2269  nfcxfr  2336  neir  2370  neirr  2376  eqnetri  2390  nesymir  2414  nelir  2465  mprgbir  2555  vex  2766  issetri  2772  moeq  2939  cdeqi  2974  ru  2988  eqsstri  3216  3sstr4i  3225  mosn  3659  rabrsndc  3691  tpid1  3734  tpid2  3736  tpid3  3739  pwv  3839  uni0  3867  eqbrtri  4055  tr0  4143  trv  4144  zfnuleu  4158  0ex  4161  inex1  4168  elpwi2  4192  0elpw  4198  axpow2  4210  axpow3  4211  vpwex  4213  zfpair2  4244  exss  4261  moop2  4285  pwundifss  4321  po0  4347  epse  4378  fr0  4387  0elon  4428  onm  4437  uniex2  4472  snnex  4484  ordtriexmidlem  4556  ordtriexmid  4558  ontr2exmid  4562  ordtri2or2exmidlem  4563  onsucsssucexmid  4564  onsucelsucexmidlem  4566  ruALT  4588  zfregfr  4611  dcextest  4618  zfinf2  4626  omex  4630  finds  4637  finds2  4638  ordom  4644  omsinds  4659  relsnop  4770  relxp  4773  rel0  4789  relopabiv  4790  relopabi  4792  eliunxp  4806  opeliunxp2  4807  dmi  4882  xpidtr  5061  cnvcnv  5123  dmsn0  5138  cnvsn0  5139  funmpt  5297  funmpt2  5298  funinsn  5308  isarep2  5346  f0  5451  f10  5541  f1o00  5542  f1oi  5545  f1osn  5547  brprcneu  5554  fvopab3ig  5638  opabex  5789  eufnfv  5796  mpofun  6028  reldmmpo  6038  ovid  6043  ovidig  6044  ovidi  6045  ovig  6048  ovi3  6064  oprabex  6194  oprabex3  6195  f1stres  6226  f2ndres  6227  opeliunxp2f  6305  tpos0  6341  issmo  6355  tfrlem6  6383  tfrlem8  6385  tfri1dALT  6418  tfrcl  6431  rdgfun  6440  frecfun  6462  frecfcllem  6471  0lt1o  6507  eqer  6633  ecopover  6701  ecopoverg  6704  th3qcor  6707  mapsnf1o3  6765  ssdomg  6846  ensn1  6864  xpcomf1o  6893  fiunsnnn  6951  finexdc  6972  exmidpw  6978  dcfi  7056  omct  7192  infnninf  7199  infnninfOLD  7200  pm54.43  7269  exmidonfinlem  7272  pw1on  7309  pw1dom2  7310  pw1ne1  7312  2oneel  7339  dmaddpi  7409  dmmulpi  7410  1lt2pi  7424  indpi  7426  1lt2nq  7490  genpelxp  7595  ltexprlempr  7692  recexprlempr  7716  cauappcvgprlemcl  7737  cauappcvgprlemladd  7742  caucvgprlemcl  7760  caucvgprprlemcl  7788  m1p1sr  7844  m1m1sr  7845  0lt1sr  7849  peano1nnnn  7936  ax1cn  7945  ax1re  7946  axaddf  7952  axmulf  7953  ax0lt1  7960  0lt1  8170  subaddrii  8332  ixi  8627  1ap0  8634  sup3exmid  9001  nn1suc  9026  neg1lt0  9115  4d2e2  9168  iap0  9231  un0mulcl  9300  pnf0xnn0  9336  3halfnz  9440  nummac  9518  uzf  9621  mnfltpnf  9877  ixxf  9990  ioof  10063  fzf  10104  fzp1disj  10172  fzp1nel  10196  fzo0  10261  frecfzennn  10535  frechashgf1o  10537  xnn0nnen  10546  fxnn0nninf  10548  seq3f1olemp  10624  sq0  10739  irec  10748  hash0  10905  prhash2ex  10918  climmo  11480  sum0  11570  fisumcom2  11620  prod0  11767  fprodcom2fi  11808  cos1bnd  11941  cos2bnd  11942  3dvds  12046  n2dvdsm1  12095  n2dvds3  12097  flodddiv4  12118  3lcm2e6woprm  12279  6lcm4e12  12280  2prm  12320  3lcm2e6  12353  pockthi  12552  modsubi  12613  unennn  12639  ssnnctlemct  12688  structcnvcnv  12719  strleun  12807  starvndxnbasendx  12844  starvndxnplusgndx  12845  starvndxnmulrndx  12846  scandxnbasendx  12856  scandxnplusgndx  12857  scandxnmulrndx  12858  vscandxnbasendx  12861  vscandxnplusgndx  12862  vscandxnmulrndx  12863  vscandxnscandx  12864  ipndxnbasendx  12874  ipndxnplusgndx  12875  ipndxnmulrndx  12876  slotsdifipndx  12877  tsetndxnplusgndx  12894  tsetndxnmulrndx  12895  tsetndxnstarvndx  12896  slotstnscsi  12897  plendxnplusgndx  12908  plendxnmulrndx  12909  plendxnscandx  12910  plendxnvscandx  12911  slotsdifplendx  12912  basendxnocndx  12915  plendxnocndx  12916  dsndxnplusgndx  12923  dsndxnmulrndx  12924  slotsdnscsi  12925  dsndxntsetndx  12926  slotsdifdsndx  12927  unifndxntsetndx  12933  slotsdifunifndx  12934  restid  12952  prdsval  12975  mgmidmo  13074  rrgmex  13893  lssmex  13987  lidlmex  14107  2idlmex  14133  fczpsrbag  14301  tgdom  14392  tgidm  14394  resttopon  14491  rest0  14499  psmetrel  14642  metrel  14662  xmetrel  14663  xmetf  14670  0met  14704  mopnrel  14761  setsmsbasg  14799  setsmsdsg  14800  qtopbasss  14841  reldvg  14999  dvexp  15031  dveflem  15046  elply2  15055  elplyd  15061  ply1term  15063  plymullem  15070  efcn  15088  sinhalfpilem  15111  sincosq1lem  15145  tangtx  15158  sincos4thpi  15160  pigt3  15164  dfrelog  15180  relogf1o  15181  log1  15186  loge  15187  relogiso  15193  2logb9irr  15291  2logb9irrap  15297  2sqlem9  15449  2sqlem10  15450  ex-fl  15455  bj-nndcALT  15488  bj-axempty  15623  bj-axempty2  15624  bdinex1  15629  bj-zfpair2  15640  bj-uniex2  15646  bj-indint  15661  bj-omind  15664  bj-omex  15672  bj-omelon  15691  0nninf  15735  dceqnconst  15791  dcapnconst  15792