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

Theorem simprbi 260
Description: Deduction eliminating a conjunct. (Contributed by NM, 27-May-1998.)
Hypothesis
Ref Expression
simprbi.1 (φ ↔ (ψ χ))
Assertion
Ref Expression
simprbi (φχ)

Proof of Theorem simprbi
StepHypRef Expression
1 simprbi.1 . . 3 (φ ↔ (ψ χ))
21biimpi 113 . 2 (φ → (ψ χ))
32simprd 107 1 (φχ)
Colors of variables: wff set class
Syntax hints:  wi 4   wa 97  wb 98
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100
This theorem depends on definitions:  df-bi 110
This theorem is referenced by:  pm5.63dc  852  sb1  1646  reurmo  2518  pssne  3034  pssn2lp  3039  ssnpss  3041  eldifn  3061  disj4im  3270  rabsnt  3436  eldifsni  3487  unimax  3605  ssintub  3624  moop2  3979  trssord  4083  ordelord  4084  ordsucim  4192  regexmidlem1  4218  tfis  4249  opelxp2  4321  funmo  4860  funopg  4877  funco  4883  funun  4887  fununi  4910  funimaexglem  4925  fndm  4941  frn  4995  f1ss  5040  f1ssr  5041  f1ssres  5042  forn  5052  f1f1orn  5080  f1orescnv  5085  f1imacnv  5086  funcocnv2  5094  funfveu  5131  nfvres  5149  foelrn  5260  isorel  5391  isoini2  5401  f1ofveu  5443  fovcl  5548  f1opw  5649  f1o2ndf1  5791  mpt2xopn0yelv  5795  swoer  6070  en0  6211  en1  6215  ssfiexmid  6254  0npi  6297  mulclpi  6312  mulcanpig  6319  nlt1pig  6325  indpi  6326  nnppipi  6327  dfplpq2  6338  archnqq  6400  enq0tr  6416  nqnq0pi  6420  ltexprlemopl  6574  ltexprlemopu  6576  cauappcvgprlemopl  6617  cauappcvgprlemlol  6618  cauappcvgprlemopu  6619  cauappcvgprlemupu  6620  cauappcvgprlemdisj  6622  ltresr2  6717  axrnegex  6743  ltxrlt  6862  peano2nn  7687  elnn0z  8014  zaddcl  8041  ztri3or0  8043  1nuz2  8299  rpgt0  8349  ixxss1  8523  ixxss2  8524  ixxss12  8525  iccss2  8563  iccssico2  8566  elfzuz3  8637  uzdisj  8705  nn0disj  8745  expge0  8925  expge1  8926  expaddzaplem  8932  bj-indsuc  9363
  Copyright terms: Public domain W3C validator