ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  mpbir Unicode 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  |-  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 128 . 2  |-  ( ps 
->  ph )
41, 3ax-mp 7 1  |-  ph
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  635  stabnot  752  mpbir2an  860  mpbir3an  1097  tru  1263  mpgbir  1358  nfxfr  1379  19.8a  1498  sbt  1683  dveeq2  1712  dveeq2or  1713  sbequilem  1735  cbvex2  1813  dvelimALT  1902  dvelimfv  1903  dvelimor  1910  nfeuv  1934  moaneu  1992  moanmo  1993  eqeltri  2126  nfcxfr  2191  neir  2223  neirr  2229  eqnetri  2243  nesymir  2267  nelir  2317  mprgbir  2396  vex  2577  issetri  2581  moeq  2739  cdeqi  2772  ru  2786  eqsstri  3003  3sstr4i  3012  rgenm  3351  mosn  3434  rabrsndc  3466  tpid1  3509  tpid2  3510  tpid3  3512  pwv  3607  uni0  3635  eqbrtri  3811  tr0  3893  trv  3894  zfnuleu  3909  0ex  3912  inex1  3919  0elpw  3945  axpow2  3957  axpow3  3958  pwex  3960  zfpair2  3973  exss  3991  moop2  4016  pwundifss  4050  po0  4076  epse  4107  fr0  4116  0elon  4157  onm  4166  uniex2  4201  snnex  4209  ordtriexmidlem  4273  ordtriexmid  4275  ontr2exmid  4278  ordtri2or2exmidlem  4279  onsucsssucexmid  4280  onsucelsucexmidlem  4282  ruALT  4303  zfregfr  4326  zfinf2  4340  omex  4344  finds  4351  finds2  4352  ordom  4357  relsnop  4472  relxp  4475  rel0  4490  relopabi  4491  eliunxp  4503  opeliunxp2  4504  dmi  4578  xpidtr  4743  cnvcnv  4801  dmsn0  4816  cnvsn0  4817  funmpt  4966  funmpt2  4967  isarep2  5014  f0  5108  f10  5188  f1o00  5189  f1oi  5192  f1osn  5194  brprcneu  5199  fvopab3ig  5274  opabex  5413  eufnfv  5417  mpt2fun  5631  reldmmpt2  5640  ovid  5645  ovidig  5646  ovidi  5647  ovig  5650  ovi3  5665  oprabex  5783  oprabex3  5784  f1stres  5814  f2ndres  5815  tpos0  5920  issmo  5934  tfrlem6  5963  tfrlem8  5965  rdgfun  5991  0lt1o  6054  eqer  6169  ecopover  6235  ecopoverg  6238  th3qcor  6241  ssdomg  6289  ensn1  6307  xpcomf1o  6330  fiunsnnn  6369  dmaddpi  6481  dmmulpi  6482  1lt2pi  6496  indpi  6498  1lt2nq  6562  genpelxp  6667  ltexprlempr  6764  recexprlempr  6788  cauappcvgprlemcl  6809  cauappcvgprlemladd  6814  caucvgprlemcl  6832  caucvgprprlemcl  6860  m1p1sr  6903  m1m1sr  6904  0lt1sr  6908  peano1nnnn  6986  ax1cn  6995  ax1re  6996  ax0lt1  7008  ax-0lt1  7048  0lt1  7202  subaddrii  7363  ixi  7648  1ap0  7655  nn1suc  8009  neg1lt0  8098  4d2e2  8143  iap0  8205  un0mulcl  8273  3halfnz  8395  nummac  8471  uzf  8572  mnfltpnf  8807  ixxf  8868  ioof  8941  fzf  8980  fzp1disj  9044  fzp1nel  9068  fzo0  9126  frecfzennn  9367  frechashgf1o  9369  sq0  9510  irec  9518  climmo  10050  n2dvdsm1  10225  n2dvds3  10227  flodddiv4  10246  ex-fl  10279  bj-axempty  10400  bj-axempty2  10401  bdinex1  10406  bj-zfpair2  10417  bj-uniex2  10423  bj-indint  10442  bj-omind  10445  bj-omex  10454  bj-omelon  10473
  Copyright terms: Public domain W3C validator