ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  mpbir GIF 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 𝜓
mpbir.maj (𝜑𝜓)
Assertion
Ref Expression
mpbir 𝜑

Proof of Theorem mpbir
StepHypRef Expression
1 mpbir.min . 2 𝜓
2 mpbir.maj . . 3 (𝜑𝜓)
32biimpri 132 . 2 (𝜓𝜑)
41, 3ax-mp 5 1 𝜑
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  680  stabnot  818  mpbir2an  926  mpbir3an  1163  tru  1335  mpgbir  1429  nfxfr  1450  19.8a  1569  sbt  1757  dveeq2  1787  dveeq2or  1788  sbequilem  1810  cbvex2  1894  dvelimALT  1985  dvelimfv  1986  dvelimor  1993  nfeuv  2017  moaneu  2075  moanmo  2076  eqeltri  2212  nfcxfr  2278  neir  2311  neirr  2317  eqnetri  2331  nesymir  2355  nelir  2406  mprgbir  2490  vex  2689  issetri  2695  moeq  2859  cdeqi  2894  ru  2908  eqsstri  3129  3sstr4i  3138  rgenm  3465  mosn  3560  rabrsndc  3591  tpid1  3634  tpid2  3636  tpid3  3639  pwv  3735  uni0  3763  eqbrtri  3949  tr0  4037  trv  4038  zfnuleu  4052  0ex  4055  inex1  4062  0elpw  4088  axpow2  4100  axpow3  4101  vpwex  4103  zfpair2  4132  exss  4149  moop2  4173  pwundifss  4207  po0  4233  epse  4264  fr0  4273  0elon  4314  onm  4323  uniex2  4358  snnex  4369  ordtriexmidlem  4435  ordtriexmid  4437  ontr2exmid  4440  ordtri2or2exmidlem  4441  onsucsssucexmid  4442  onsucelsucexmidlem  4444  ruALT  4466  zfregfr  4488  dcextest  4495  zfinf2  4503  omex  4507  finds  4514  finds2  4515  ordom  4520  omsinds  4535  relsnop  4645  relxp  4648  rel0  4664  relopabi  4665  eliunxp  4678  opeliunxp2  4679  dmi  4754  xpidtr  4929  cnvcnv  4991  dmsn0  5006  cnvsn0  5007  funmpt  5161  funmpt2  5162  funinsn  5172  isarep2  5210  f0  5313  f10  5401  f1o00  5402  f1oi  5405  f1osn  5407  brprcneu  5414  fvopab3ig  5495  opabex  5644  eufnfv  5648  mpofun  5873  reldmmpo  5882  ovid  5887  ovidig  5888  ovidi  5889  ovig  5892  ovi3  5907  oprabex  6026  oprabex3  6027  f1stres  6057  f2ndres  6058  opeliunxp2f  6135  tpos0  6171  issmo  6185  tfrlem6  6213  tfrlem8  6215  tfri1dALT  6248  tfrcl  6261  rdgfun  6270  frecfun  6292  frecfcllem  6301  0lt1o  6337  eqer  6461  ecopover  6527  ecopoverg  6530  th3qcor  6533  mapsnf1o3  6591  ssdomg  6672  ensn1  6690  xpcomf1o  6719  fiunsnnn  6775  finexdc  6796  exmidpw  6802  omct  7002  infnninf  7022  nnnninf  7023  pm54.43  7051  exmidonfinlem  7054  dmaddpi  7145  dmmulpi  7146  1lt2pi  7160  indpi  7162  1lt2nq  7226  genpelxp  7331  ltexprlempr  7428  recexprlempr  7452  cauappcvgprlemcl  7473  cauappcvgprlemladd  7478  caucvgprlemcl  7496  caucvgprprlemcl  7524  m1p1sr  7580  m1m1sr  7581  0lt1sr  7585  peano1nnnn  7672  ax1cn  7681  ax1re  7682  axaddf  7688  axmulf  7689  ax0lt1  7696  0lt1  7901  subaddrii  8063  ixi  8357  1ap0  8364  sup3exmid  8727  nn1suc  8751  neg1lt0  8840  4d2e2  8892  iap0  8955  un0mulcl  9023  pnf0xnn0  9059  3halfnz  9160  nummac  9238  uzf  9341  mnfltpnf  9583  ixxf  9693  ioof  9766  fzf  9806  fzp1disj  9872  fzp1nel  9896  fzo0  9957  frecfzennn  10211  frechashgf1o  10213  fxnn0nninf  10223  seq3f1olemp  10287  sq0  10395  irec  10404  hash0  10555  prhash2ex  10567  climmo  11079  sum0  11169  fisumcom2  11219  cos1bnd  11477  cos2bnd  11478  n2dvdsm1  11621  n2dvds3  11623  flodddiv4  11642  3lcm2e6woprm  11778  6lcm4e12  11779  2prm  11819  3lcm2e6  11849  unennn  11921  structcnvcnv  11989  strleun  12062  restid  12145  tgdom  12255  tgidm  12257  resttopon  12354  rest0  12362  psmetrel  12505  metrel  12525  xmetrel  12526  xmetf  12533  0met  12567  mopnrel  12624  setsmsbasg  12662  setsmsdsg  12663  qtopbasss  12704  reldvg  12831  dvexp  12858  dveflem  12870  efcn  12872  sinhalfpilem  12894  sincosq1lem  12928  tangtx  12941  sincos4thpi  12943  pigt3  12947  dfrelog  12963  relogf1o  12964  log1  12969  loge  12970  relogiso  12976  ex-fl  13021  bj-nndcALT  13047  bj-axempty  13175  bj-axempty2  13176  bdinex1  13181  bj-zfpair2  13192  bj-uniex2  13198  bj-indint  13213  bj-omind  13216  bj-omex  13224  bj-omelon  13243  pw1dom2  13274  0nninf  13283
  Copyright terms: Public domain W3C validator