ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  mpbir Unicode version

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
StepHypRef Expression
1 mpbir.min . 2  |-  ps
2 mpbir.maj . . 3  |-  ( ph  <->  ps )
32biimpri 132 . 2  |-  ( ps 
->  ph )
41, 3ax-mp 5 1  |-  ph
Colors of variables: wff set class
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  665  stabnot  803  mpbir2an  911  mpbir3an  1148  tru  1320  mpgbir  1414  nfxfr  1435  19.8a  1554  sbt  1742  dveeq2  1771  dveeq2or  1772  sbequilem  1794  cbvex2  1874  dvelimALT  1963  dvelimfv  1964  dvelimor  1971  nfeuv  1995  moaneu  2053  moanmo  2054  eqeltri  2190  nfcxfr  2255  neir  2288  neirr  2294  eqnetri  2308  nesymir  2332  nelir  2383  mprgbir  2467  vex  2663  issetri  2669  moeq  2832  cdeqi  2867  ru  2881  eqsstri  3099  3sstr4i  3108  rgenm  3435  mosn  3530  rabrsndc  3561  tpid1  3604  tpid2  3606  tpid3  3609  pwv  3705  uni0  3733  eqbrtri  3919  tr0  4007  trv  4008  zfnuleu  4022  0ex  4025  inex1  4032  0elpw  4058  axpow2  4070  axpow3  4071  vpwex  4073  zfpair2  4102  exss  4119  moop2  4143  pwundifss  4177  po0  4203  epse  4234  fr0  4243  0elon  4284  onm  4293  uniex2  4328  snnex  4339  ordtriexmidlem  4405  ordtriexmid  4407  ontr2exmid  4410  ordtri2or2exmidlem  4411  onsucsssucexmid  4412  onsucelsucexmidlem  4414  ruALT  4436  zfregfr  4458  dcextest  4465  zfinf2  4473  omex  4477  finds  4484  finds2  4485  ordom  4490  omsinds  4505  relsnop  4615  relxp  4618  rel0  4634  relopabi  4635  eliunxp  4648  opeliunxp2  4649  dmi  4724  xpidtr  4899  cnvcnv  4961  dmsn0  4976  cnvsn0  4977  funmpt  5131  funmpt2  5132  funinsn  5142  isarep2  5180  f0  5283  f10  5369  f1o00  5370  f1oi  5373  f1osn  5375  brprcneu  5382  fvopab3ig  5463  opabex  5612  eufnfv  5616  mpofun  5841  reldmmpo  5850  ovid  5855  ovidig  5856  ovidi  5857  ovig  5860  ovi3  5875  oprabex  5994  oprabex3  5995  f1stres  6025  f2ndres  6026  opeliunxp2f  6103  tpos0  6139  issmo  6153  tfrlem6  6181  tfrlem8  6183  tfri1dALT  6216  tfrcl  6229  rdgfun  6238  frecfun  6260  frecfcllem  6269  0lt1o  6305  eqer  6429  ecopover  6495  ecopoverg  6498  th3qcor  6501  mapsnf1o3  6559  ssdomg  6640  ensn1  6658  xpcomf1o  6687  fiunsnnn  6743  finexdc  6764  exmidpw  6770  omct  6970  infnninf  6990  nnnninf  6991  pm54.43  7014  exmidonfinlem  7017  dmaddpi  7101  dmmulpi  7102  1lt2pi  7116  indpi  7118  1lt2nq  7182  genpelxp  7287  ltexprlempr  7384  recexprlempr  7408  cauappcvgprlemcl  7429  cauappcvgprlemladd  7434  caucvgprlemcl  7452  caucvgprprlemcl  7480  m1p1sr  7536  m1m1sr  7537  0lt1sr  7541  peano1nnnn  7628  ax1cn  7637  ax1re  7638  axaddf  7644  axmulf  7645  ax0lt1  7652  0lt1  7857  subaddrii  8019  ixi  8313  1ap0  8320  sup3exmid  8683  nn1suc  8707  neg1lt0  8796  4d2e2  8848  iap0  8911  un0mulcl  8979  pnf0xnn0  9015  3halfnz  9116  nummac  9194  uzf  9297  mnfltpnf  9539  ixxf  9649  ioof  9722  fzf  9762  fzp1disj  9828  fzp1nel  9852  fzo0  9913  frecfzennn  10167  frechashgf1o  10169  fxnn0nninf  10179  seq3f1olemp  10243  sq0  10351  irec  10360  hash0  10511  prhash2ex  10523  climmo  11035  sum0  11125  fisumcom2  11175  cos1bnd  11393  cos2bnd  11394  n2dvdsm1  11537  n2dvds3  11539  flodddiv4  11558  3lcm2e6woprm  11694  6lcm4e12  11695  2prm  11735  3lcm2e6  11765  unennn  11837  structcnvcnv  11902  strleun  11975  restid  12058  tgdom  12168  tgidm  12170  resttopon  12267  rest0  12275  psmetrel  12418  metrel  12438  xmetrel  12439  xmetf  12446  0met  12480  mopnrel  12537  setsmsbasg  12575  setsmsdsg  12576  qtopbasss  12617  reldvg  12744  dvexp  12771  dveflem  12782  efcn  12784  sinhalfpilem  12799  sincosq1lem  12833  tangtx  12846  sincos4thpi  12848  pigt3  12852  ex-fl  12864  bj-nndcALT  12890  bj-axempty  13018  bj-axempty2  13019  bdinex1  13024  bj-zfpair2  13035  bj-uniex2  13041  bj-indint  13056  bj-omind  13059  bj-omex  13067  bj-omelon  13086  pw1dom2  13117  0nninf  13124
  Copyright terms: Public domain W3C validator