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

Theorem mpbir 144
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 131 . 2 (𝜓𝜑)
41, 3ax-mp 7 1 𝜑
Colors of variables: wff set class
Syntax hints:  wb 103
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106
This theorem depends on definitions:  df-bi 115
This theorem is referenced by:  pm5.74ri  179  imnani  658  stabnot  775  mpbir2an  884  mpbir3an  1121  tru  1289  mpgbir  1383  nfxfr  1404  19.8a  1523  sbt  1708  dveeq2  1737  dveeq2or  1738  sbequilem  1760  cbvex2  1839  dvelimALT  1928  dvelimfv  1929  dvelimor  1936  nfeuv  1960  moaneu  2018  moanmo  2019  eqeltri  2152  nfcxfr  2217  neir  2249  neirr  2255  eqnetri  2269  nesymir  2293  nelir  2343  mprgbir  2422  vex  2605  issetri  2609  moeq  2768  cdeqi  2801  ru  2815  eqsstri  3030  3sstr4i  3039  rgenm  3345  mosn  3431  rabrsndc  3462  tpid1  3505  tpid2  3506  tpid3  3508  pwv  3602  uni0  3630  eqbrtri  3806  tr0  3888  trv  3889  zfnuleu  3904  0ex  3907  inex1  3914  0elpw  3940  axpow2  3952  axpow3  3953  pwex  3955  zfpair2  3967  exss  3984  moop2  4008  pwundifss  4042  po0  4068  epse  4099  fr0  4108  0elon  4149  onm  4158  uniex2  4193  snnex  4201  ordtriexmidlem  4265  ordtriexmid  4267  ontr2exmid  4270  ordtri2or2exmidlem  4271  onsucsssucexmid  4272  onsucelsucexmidlem  4274  ruALT  4296  zfregfr  4318  zfinf2  4332  omex  4336  finds  4343  finds2  4344  ordom  4349  relsnop  4466  relxp  4469  rel0  4484  relopabi  4485  eliunxp  4497  opeliunxp2  4498  dmi  4572  xpidtr  4739  cnvcnv  4797  dmsn0  4812  cnvsn0  4813  funmpt  4962  funmpt2  4963  funinsn  4973  isarep2  5011  f0  5105  f10  5185  f1o00  5186  f1oi  5189  f1osn  5191  brprcneu  5196  fvopab3ig  5272  opabex  5411  eufnfv  5415  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  5959  tfrlem8  5961  tfri1dALT  5994  tfrcl  6007  rdgfun  6016  frecfun  6038  frecfcllem  6047  0lt1o  6081  eqer  6197  ecopover  6263  ecopoverg  6266  th3qcor  6269  ssdomg  6317  ensn1  6335  xpcomf1o  6359  fiunsnnn  6405  pm54.43  6508  dmaddpi  6566  dmmulpi  6567  1lt2pi  6581  indpi  6583  1lt2nq  6647  genpelxp  6752  ltexprlempr  6849  recexprlempr  6873  cauappcvgprlemcl  6894  cauappcvgprlemladd  6899  caucvgprlemcl  6917  caucvgprprlemcl  6945  m1p1sr  6988  m1m1sr  6989  0lt1sr  6993  peano1nnnn  7071  ax1cn  7080  ax1re  7081  ax0lt1  7093  0lt1  7292  subaddrii  7453  ixi  7739  1ap0  7746  nn1suc  8114  neg1lt0  8203  4d2e2  8248  iap0  8310  un0mulcl  8378  pnf0xnn0  8414  3halfnz  8514  nummac  8591  uzf  8692  mnfltpnf  8925  ixxf  8986  ioof  9059  fzf  9098  fzp1disj  9162  fzp1nel  9186  fzo0  9243  frecfzennn  9497  frechashgf1o  9499  sq0  9652  irec  9660  size0  9810  prsize2ex  9822  climmo  10264  n2dvdsm1  10446  n2dvds3  10448  flodddiv4  10467  3lcm2e6woprm  10601  6lcm4e12  10602  2prm  10642  3lcm2e6  10672  ex-fl  10699  bj-axempty  10827  bj-axempty2  10828  bdinex1  10833  bj-zfpair2  10844  bj-uniex2  10850  bj-indint  10869  bj-omind  10872  bj-omex  10880  bj-omelon  10899
  Copyright terms: Public domain W3C validator