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  663  stabnot  801  mpbir2an  909  mpbir3an  1146  tru  1318  mpgbir  1412  nfxfr  1433  19.8a  1552  sbt  1740  dveeq2  1769  dveeq2or  1770  sbequilem  1792  cbvex2  1872  dvelimALT  1961  dvelimfv  1962  dvelimor  1969  nfeuv  1993  moaneu  2051  moanmo  2052  eqeltri  2188  nfcxfr  2253  neir  2286  neirr  2292  eqnetri  2306  nesymir  2330  nelir  2381  mprgbir  2465  vex  2661  issetri  2667  moeq  2830  cdeqi  2865  ru  2879  eqsstri  3097  3sstr4i  3106  rgenm  3433  mosn  3528  rabrsndc  3559  tpid1  3602  tpid2  3604  tpid3  3607  pwv  3703  uni0  3731  eqbrtri  3917  tr0  4005  trv  4006  zfnuleu  4020  0ex  4023  inex1  4030  0elpw  4056  axpow2  4068  axpow3  4069  vpwex  4071  zfpair2  4100  exss  4117  moop2  4141  pwundifss  4175  po0  4201  epse  4232  fr0  4241  0elon  4282  onm  4291  uniex2  4326  snnex  4337  ordtriexmidlem  4403  ordtriexmid  4405  ontr2exmid  4408  ordtri2or2exmidlem  4409  onsucsssucexmid  4410  onsucelsucexmidlem  4412  ruALT  4434  zfregfr  4456  dcextest  4463  zfinf2  4471  omex  4475  finds  4482  finds2  4483  ordom  4488  omsinds  4503  relsnop  4613  relxp  4616  rel0  4632  relopabi  4633  eliunxp  4646  opeliunxp2  4647  dmi  4722  xpidtr  4897  cnvcnv  4959  dmsn0  4974  cnvsn0  4975  funmpt  5129  funmpt2  5130  funinsn  5140  isarep2  5178  f0  5281  f10  5367  f1o00  5368  f1oi  5371  f1osn  5373  brprcneu  5380  fvopab3ig  5461  opabex  5610  eufnfv  5614  mpofun  5839  reldmmpo  5848  ovid  5853  ovidig  5854  ovidi  5855  ovig  5858  ovi3  5873  oprabex  5992  oprabex3  5993  f1stres  6023  f2ndres  6024  opeliunxp2f  6101  tpos0  6137  issmo  6151  tfrlem6  6179  tfrlem8  6181  tfri1dALT  6214  tfrcl  6227  rdgfun  6236  frecfun  6258  frecfcllem  6267  0lt1o  6303  eqer  6427  ecopover  6493  ecopoverg  6496  th3qcor  6499  mapsnf1o3  6557  ssdomg  6638  ensn1  6656  xpcomf1o  6685  fiunsnnn  6741  finexdc  6762  exmidpw  6768  omct  6968  infnninf  6988  nnnninf  6989  pm54.43  7012  dmaddpi  7097  dmmulpi  7098  1lt2pi  7112  indpi  7114  1lt2nq  7178  genpelxp  7283  ltexprlempr  7380  recexprlempr  7404  cauappcvgprlemcl  7425  cauappcvgprlemladd  7430  caucvgprlemcl  7448  caucvgprprlemcl  7476  m1p1sr  7532  m1m1sr  7533  0lt1sr  7537  peano1nnnn  7624  ax1cn  7633  ax1re  7634  axaddf  7640  axmulf  7641  ax0lt1  7648  0lt1  7853  subaddrii  8015  ixi  8308  1ap0  8315  sup3exmid  8675  nn1suc  8699  neg1lt0  8788  4d2e2  8834  iap0  8897  un0mulcl  8965  pnf0xnn0  9001  3halfnz  9102  nummac  9180  uzf  9281  mnfltpnf  9522  ixxf  9632  ioof  9705  fzf  9745  fzp1disj  9811  fzp1nel  9835  fzo0  9896  frecfzennn  10150  frechashgf1o  10152  fxnn0nninf  10162  seq3f1olemp  10226  sq0  10334  irec  10343  hash0  10494  prhash2ex  10506  climmo  11018  sum0  11108  fisumcom2  11158  cos1bnd  11376  cos2bnd  11377  n2dvdsm1  11517  n2dvds3  11519  flodddiv4  11538  3lcm2e6woprm  11674  6lcm4e12  11675  2prm  11715  3lcm2e6  11745  unennn  11816  structcnvcnv  11881  strleun  11954  restid  12037  tgdom  12147  tgidm  12149  resttopon  12246  rest0  12254  psmetrel  12397  metrel  12417  xmetrel  12418  xmetf  12425  0met  12459  mopnrel  12516  setsmsbasg  12554  setsmsdsg  12555  qtopbasss  12596  reldvg  12723  dvexp  12750  dveflem  12761  efcn  12763  ex-fl  12771  bj-nndcALT  12797  bj-axempty  12925  bj-axempty2  12926  bdinex1  12931  bj-zfpair2  12942  bj-uniex2  12948  bj-indint  12963  bj-omind  12966  bj-omex  12974  bj-omelon  12993  pw1dom2  13024  0nninf  13031
  Copyright terms: Public domain W3C validator