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  693  stabnot  835  mpbir2an  945  mpbir3an  1182  tru  1377  dcfromnotnotr  1468  dcfromcon  1469  dcfrompeirce  1470  mpgbir  1477  nfxfr  1498  19.8a  1614  sbt  1808  dveeq2  1839  dveeq2or  1840  sbequilem  1862  cbvex2  1947  dvelimALT  2039  dvelimfv  2040  dvelimor  2047  nfeuv  2073  moaneu  2131  moanmo  2132  eqeltri  2279  nfcxfr  2346  neir  2380  neirr  2386  eqnetri  2400  nesymir  2424  nelir  2475  mprgbir  2565  vex  2776  issetri  2783  moeq  2952  cdeqi  2987  ru  3001  eqsstri  3229  3sstr4i  3238  mosn  3674  rabrsndc  3706  tpid1  3749  tpid2  3751  tpid3  3754  pwv  3858  uni0  3886  eqbrtri  4075  tr0  4164  trv  4165  zfnuleu  4179  0ex  4182  inex1  4189  elpwi2  4213  0elpw  4219  axpow2  4231  axpow3  4232  vpwex  4234  zfpair2  4265  exss  4284  opwo0id  4306  moop2  4309  pwundifss  4345  po0  4371  epse  4402  fr0  4411  0elon  4452  onm  4461  uniex2  4496  snnex  4508  ordtriexmidlem  4580  ordtriexmid  4582  ontr2exmid  4586  ordtri2or2exmidlem  4587  onsucsssucexmid  4588  onsucelsucexmidlem  4590  ruALT  4612  zfregfr  4635  dcextest  4642  zfinf2  4650  omex  4654  finds  4661  finds2  4662  ordom  4668  omsinds  4683  relsnop  4794  relxp  4797  rel0  4813  relopabiv  4814  relopabi  4816  eliunxp  4830  opeliunxp2  4831  dmi  4907  xpidtr  5087  cnvcnv  5149  dmsn0  5164  cnvsn0  5165  funmpt  5323  funmpt2  5324  funinsn  5337  isarep2  5375  f0  5483  f10  5573  f10d  5574  f1o00  5575  f1oi  5578  f1osn  5580  brprcneu  5587  fvopab3ig  5671  opabex  5826  eufnfv  5833  mpofun  6065  reldmmpo  6075  ovid  6080  ovidig  6081  ovidi  6082  ovig  6085  ovi3  6101  oprabex  6231  oprabex3  6232  f1stres  6263  f2ndres  6264  opeliunxp2f  6342  tpos0  6378  issmo  6392  tfrlem6  6420  tfrlem8  6422  tfri1dALT  6455  tfrcl  6468  rdgfun  6477  frecfun  6499  frecfcllem  6508  0lt1o  6544  eqer  6670  ecopover  6738  ecopoverg  6741  th3qcor  6744  mapsnf1o3  6802  ssdomg  6888  ensn1  6906  xpcomf1o  6940  fiunsnnn  6999  finexdc  7020  exmidpw  7026  dcfi  7104  omct  7240  infnninf  7247  infnninfOLD  7248  pm54.43  7319  exmidonfinlem  7327  pw1on  7367  pw1dom2  7368  pw1ne1  7370  2oneel  7398  dmaddpi  7468  dmmulpi  7469  1lt2pi  7483  indpi  7485  1lt2nq  7549  genpelxp  7654  ltexprlempr  7751  recexprlempr  7775  cauappcvgprlemcl  7796  cauappcvgprlemladd  7801  caucvgprlemcl  7819  caucvgprprlemcl  7847  m1p1sr  7903  m1m1sr  7904  0lt1sr  7908  peano1nnnn  7995  ax1cn  8004  ax1re  8005  axaddf  8011  axmulf  8012  ax0lt1  8019  0lt1  8229  subaddrii  8391  ixi  8686  1ap0  8693  sup3exmid  9060  nn1suc  9085  neg1lt0  9174  4d2e2  9227  iap0  9290  un0mulcl  9359  pnf0xnn0  9395  3halfnz  9500  nummac  9578  uzf  9681  mnfltpnf  9937  ixxf  10050  ioof  10123  fzf  10164  fzp1disj  10232  fzp1nel  10256  fzo0  10322  frecfzennn  10603  frechashgf1o  10605  xnn0nnen  10614  fxnn0nninf  10616  seq3f1olemp  10692  sq0  10807  irec  10816  hash0  10973  prhash2ex  10986  climmo  11694  sum0  11784  fisumcom2  11834  prod0  11981  fprodcom2fi  12022  cos1bnd  12155  cos2bnd  12156  3dvds  12260  n2dvdsm1  12309  n2dvds3  12311  flodddiv4  12332  3lcm2e6woprm  12493  6lcm4e12  12494  2prm  12534  3lcm2e6  12567  pockthi  12766  modsubi  12827  unennn  12853  ssnnctlemct  12902  structcnvcnv  12933  strleun  13021  starvndxnbasendx  13059  starvndxnplusgndx  13060  starvndxnmulrndx  13061  scandxnbasendx  13071  scandxnplusgndx  13072  scandxnmulrndx  13073  vscandxnbasendx  13076  vscandxnplusgndx  13077  vscandxnmulrndx  13078  vscandxnscandx  13079  ipndxnbasendx  13089  ipndxnplusgndx  13090  ipndxnmulrndx  13091  slotsdifipndx  13092  tsetndxnplusgndx  13109  tsetndxnmulrndx  13110  tsetndxnstarvndx  13111  slotstnscsi  13112  plendxnplusgndx  13123  plendxnmulrndx  13124  plendxnscandx  13125  plendxnvscandx  13126  slotsdifplendx  13127  basendxnocndx  13130  plendxnocndx  13131  dsndxnplusgndx  13138  dsndxnmulrndx  13139  slotsdnscsi  13140  dsndxntsetndx  13141  slotsdifdsndx  13142  unifndxntsetndx  13148  slotsdifunifndx  13149  restid  13167  prdsval  13190  mgmidmo  13289  rrgmex  14108  lssmex  14202  lidlmex  14322  2idlmex  14348  fczpsrbag  14518  tgdom  14629  tgidm  14631  resttopon  14728  rest0  14736  psmetrel  14879  metrel  14899  xmetrel  14900  xmetf  14907  0met  14941  mopnrel  14998  setsmsbasg  15036  setsmsdsg  15037  qtopbasss  15078  reldvg  15236  dvexp  15268  dveflem  15283  elply2  15292  elplyd  15298  ply1term  15300  plymullem  15307  efcn  15325  sinhalfpilem  15348  sincosq1lem  15382  tangtx  15395  sincos4thpi  15397  pigt3  15401  dfrelog  15417  relogf1o  15418  log1  15423  loge  15424  relogiso  15430  2logb9irr  15528  2logb9irrap  15534  2sqlem9  15686  2sqlem10  15687  uhgr0e  15763  uhgr0  15766  umgrbien  15791  ex-fl  15831  bj-nndcALT  15864  bj-axempty  15998  bj-axempty2  15999  bdinex1  16004  bj-zfpair2  16015  bj-uniex2  16021  bj-indint  16036  bj-omind  16039  bj-omex  16047  bj-omelon  16066  0nninf  16113  dceqnconst  16171  dcapnconst  16172