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

Theorem simprbi 264
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 117 . 2 (𝜑 → (𝜓𝜒))
32simprd 111 1 (𝜑𝜒)
Colors of variables: wff set class
Syntax hints:  wi 4  wa 101  wb 102
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 103  ax-ia2 104
This theorem depends on definitions:  df-bi 114
This theorem is referenced by:  pm5.63dc  864  sb1  1665  reurmo  2541  pssne  3068  pssn2lp  3073  ssnpss  3075  eldifn  3095  disj4im  3304  rabsnt  3473  eldifsni  3524  unimax  3642  ssintub  3661  moop2  4016  wepo  4124  wetrep  4125  trssord  4145  ordelord  4146  ordsucim  4254  ordtri2or2exmidlem  4279  regexmidlem1  4286  reg2exmidlema  4287  tfis  4334  opelxp2  4406  funmo  4945  funopg  4962  funco  4968  funun  4972  fununi  4995  funimaexglem  5010  fndm  5026  frn  5080  f1ss  5125  f1ssr  5126  f1ssres  5127  forn  5137  f1f1orn  5165  f1orescnv  5170  f1imacnv  5171  funcocnv2  5179  funfveu  5216  nfvres  5234  foelrn  5345  isorel  5476  isoini2  5486  f1ofveu  5528  fovcl  5634  f1opw  5735  f1o2ndf1  5877  mpt2xopn0yelv  5885  swoer  6165  en0  6306  en1  6310  phplem4  6349  phplem4dom  6355  phplem4on  6360  ssfiexmid  6367  diffitest  6375  supubti  6405  suplubti  6406  0npi  6469  mulclpi  6484  mulcanpig  6491  nlt1pig  6497  indpi  6498  nnppipi  6499  dfplpq2  6510  archnqq  6573  enq0tr  6590  nqnq0pi  6594  ltexprlemopl  6757  ltexprlemopu  6759  cauappcvgprlemopl  6802  cauappcvgprlemlol  6803  cauappcvgprlemopu  6804  cauappcvgprlemupu  6805  cauappcvgprlemdisj  6807  caucvgprlemopl  6825  caucvgprlemlol  6826  caucvgprlemopu  6827  caucvgprlemupu  6828  caucvgprlemdisj  6830  caucvgprprlemopl  6853  caucvgprprlemlol  6854  caucvgprprlemopu  6855  caucvgprprlemupu  6856  caucvgprprlemdisj  6858  ltresr2  6974  peano2nnnn  6987  axrnegex  7011  ltxrlt  7144  peano2nn  8002  elnn0z  8315  zaddcl  8342  ztri3or0  8344  eluz2gt1  8636  1nuz2  8640  rpgt0  8692  ixxss1  8874  ixxss2  8875  ixxss12  8876  iccss2  8914  iccssico2  8917  elfzuz3  8989  uzdisj  9057  nn0disj  9097  addmodlteq  9348  serige0  9417  expge0  9456  expge1  9457  expaddzaplem  9463  shftfn  9653  bj-indsuc  10439
  Copyright terms: Public domain W3C validator