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

Theorem mpbir 138
Description: An inference from a biconditional, related to modus ponens. (Contributed by NM, 5-Aug-1993.)
Hypotheses
Ref Expression
mpbir.min 𝜓
mpbir.maj (𝜑𝜓)
Assertion
Ref Expression
mpbir 𝜑

Proof of Theorem mpbir
StepHypRef Expression
1 mpbir.min . 2 𝜓
2 mpbir.maj . . 3 (𝜑𝜓)
32biimpri 128 . 2 (𝜓𝜑)
41, 3ax-mp 7 1 𝜑
Colors of variables: wff set class
Syntax hints:  wb 102
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 103  ax-ia2 104  ax-ia3 105
This theorem depends on definitions:  df-bi 114
This theorem is referenced by:  pm5.74ri  174  imnani  633  stabnot  750  mpbir2an  858  mpbir3an  1095  tru  1261  mpgbir  1356  nfxfr  1377  19.8a  1496  sbt  1681  dveeq2  1710  dveeq2or  1711  sbequilem  1733  cbvex2  1811  dvelimALT  1900  dvelimfv  1901  dvelimor  1908  nfeuv  1932  moaneu  1990  moanmo  1991  eqeltri  2124  nfcxfr  2189  neir  2221  neirr  2227  eqnetri  2241  nesymir  2265  nelir  2315  mprgbir  2394  vex  2575  issetri  2579  moeq  2736  cdeqi  2769  ru  2783  eqsstri  3000  3sstr4i  3009  rgenm  3348  mosn  3431  rabrsndc  3463  tpid1  3506  tpid2  3507  tpid3  3509  pwv  3604  uni0  3632  eqbrtri  3808  tr0  3890  trv  3891  zfnuleu  3906  0ex  3909  inex1  3916  0elpw  3942  axpow2  3954  axpow3  3955  pwex  3957  zfpair2  3970  exss  3988  moop2  4013  pwundifss  4047  po0  4073  epse  4104  fr0  4113  0elon  4154  onm  4163  uniex2  4198  snnex  4206  ordtriexmidlem  4270  ordtriexmid  4272  ontr2exmid  4275  ordtri2or2exmidlem  4276  onsucsssucexmid  4277  onsucelsucexmidlem  4279  ruALT  4300  zfregfr  4323  zfinf2  4337  omex  4341  finds  4348  finds2  4349  ordom  4354  relsnop  4469  relxp  4472  rel0  4487  relopabi  4488  eliunxp  4500  opeliunxp2  4501  dmi  4575  xpidtr  4740  cnvcnv  4798  dmsn0  4813  cnvsn0  4814  funmpt  4963  funmpt2  4964  isarep2  5011  f0  5105  f10  5185  f1o00  5186  f1oi  5189  f1osn  5191  brprcneu  5196  fvopab3ig  5271  opabex  5410  eufnfv  5414  mpt2fun  5628  reldmmpt2  5637  ovid  5642  ovidig  5643  ovidi  5644  ovig  5647  ovi3  5662  oprabex  5780  oprabex3  5781  f1stres  5811  f2ndres  5812  tpos0  5917  issmo  5931  tfrlem6  5960  tfrlem8  5962  rdgfun  5988  0lt1o  6051  eqer  6166  ecopover  6232  ecopoverg  6235  th3qcor  6238  ssdomg  6286  ensn1  6304  xpcomf1o  6327  fiunsnnn  6366  dmaddpi  6451  dmmulpi  6452  1lt2pi  6466  indpi  6468  1lt2nq  6532  genpelxp  6637  ltexprlempr  6734  recexprlempr  6758  cauappcvgprlemcl  6779  cauappcvgprlemladd  6784  caucvgprlemcl  6802  caucvgprprlemcl  6830  m1p1sr  6873  m1m1sr  6874  0lt1sr  6878  peano1nnnn  6956  ax1cn  6965  ax1re  6966  ax0lt1  6978  ax-0lt1  7018  0lt1  7172  subaddrii  7333  ixi  7618  1ap0  7625  nn1suc  7979  neg1lt0  8068  4d2e2  8113  iap0  8175  un0mulcl  8243  3halfnz  8365  nummac  8441  uzf  8542  mnfltpnf  8777  ixxf  8838  ioof  8911  fzf  8950  fzp1disj  9014  fzp1nel  9038  fzo0  9096  frecfzennn  9332  frechashgf1o  9334  sq0  9475  irec  9483  climmo  10013  n2dvdsm1  10188  n2dvds3  10190  ex-fl  10222  bj-axempty  10343  bj-axempty2  10344  bdinex1  10349  bj-zfpair2  10360  bj-uniex2  10366  bj-indint  10385  bj-omind  10388  bj-omex  10397  bj-omelon  10416
  Copyright terms: Public domain W3C validator