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  6417  nqnq0pi  6421  ltexprlemopl  6575  ltexprlemopu  6577  cauappcvgprlemopl  6618  cauappcvgprlemlol  6619  cauappcvgprlemopu  6620  cauappcvgprlemupu  6621  cauappcvgprlemdisj  6623  caucvgprlemopl  6640  caucvgprlemlol  6641  caucvgprlemopu  6642  caucvgprlemupu  6643  caucvgprlemdisj  6645  ltresr2  6737  axrnegex  6763  ltxrlt  6882  peano2nn  7707  elnn0z  8034  zaddcl  8061  ztri3or0  8063  1nuz2  8319  rpgt0  8369  ixxss1  8543  ixxss2  8544  ixxss12  8545  iccss2  8583  iccssico2  8586  elfzuz3  8657  uzdisj  8725  nn0disj  8765  expge0  8945  expge1  8946  expaddzaplem  8952  bj-indsuc  9387
  Copyright terms: Public domain W3C validator