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

Theorem simprbi 271
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 119 . 2 (𝜑 → (𝜓𝜒))
32simprd 113 1 (𝜑𝜒)
Colors of variables: wff set class
Syntax hints:  wi 4  wa 103  wb 104
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106
This theorem depends on definitions:  df-bi 116
This theorem is referenced by:  pm5.63dc  913  sb1  1722  reurmo  2620  eldifn  3167  elinel2  3231  rabsnt  3566  eldifsni  3620  unimax  3738  ssintub  3757  exmidsssnc  4094  moop2  4141  wepo  4249  wetrep  4250  trssord  4270  ordelord  4271  ordsucim  4384  ordtri2or2exmidlem  4409  regexmidlem1  4416  reg2exmidlema  4417  tfis  4465  opelxp2  4542  funmo  5106  funopg  5125  funco  5131  funun  5135  fununi  5159  funimaexglem  5174  fndm  5190  frn  5249  f1ss  5302  f1ssr  5303  f1ssres  5305  forn  5316  f1f1orn  5344  f1orescnv  5349  f1imacnv  5350  funcocnv2  5358  funfveu  5400  nfvres  5420  isorel  5675  isoini2  5686  f1ofveu  5728  fovcl  5842  f1opw  5943  f1o2ndf1  6091  mpoxopn0yelv  6102  swoer  6423  mapsnconst  6554  en0  6655  en1  6659  phplem4  6715  phplem4dom  6722  phplem4on  6727  ssfilem  6735  diffitest  6747  inffiexmid  6766  supubti  6852  suplubti  6853  djuinr  6914  casefun  6936  casef1  6941  djufun  6955  ctssexmid  6990  exmidfodomrlemim  7021  0npi  7085  mulclpi  7100  mulcanpig  7107  nlt1pig  7113  indpi  7114  nnppipi  7115  dfplpq2  7126  archnqq  7189  enq0tr  7206  nqnq0pi  7210  ltexprlemopl  7373  ltexprlemopu  7375  cauappcvgprlemopl  7418  cauappcvgprlemlol  7419  cauappcvgprlemopu  7420  cauappcvgprlemupu  7421  cauappcvgprlemdisj  7423  caucvgprlemopl  7441  caucvgprlemlol  7442  caucvgprlemopu  7443  caucvgprlemupu  7444  caucvgprlemdisj  7446  caucvgprprlemopl  7469  caucvgprprlemlol  7470  caucvgprprlemopu  7471  caucvgprprlemupu  7472  caucvgprprlemdisj  7474  suplocsrlempr  7579  ltresr2  7612  peano2nnnn  7625  axrnegex  7651  ltxrlt  7794  peano2nn  8689  elnn0z  9018  zaddcl  9045  ztri3or0  9047  eluz2gt1  9345  1nuz2  9349  rpgt0  9401  ixxss1  9627  ixxss2  9628  ixxss12  9629  iccss2  9667  iccssico2  9670  elfzuz3  9743  uzdisj  9813  nn0disj  9855  addmodlteq  10111  expge0  10269  expge1  10270  expaddzaplem  10276  shftfn  10536  fsumf1o  11099  fsumge0  11168  zsupcllemstep  11534  bezoutlemzz  11586  bezoutlemaz  11587  bezoutlembz  11588  bezoutlemsup  11593  1nprm  11691  nprm  11700  sqnprm  11712  dvdsprm  11713  coprm  11718  sqpweven  11748  2sqpwodd  11749  dfphi2  11791  phimullem  11796  oddennn  11800  znnen  11806  ennnfonelemg  11811  ctinf  11838  toponuni  12077  tpsuni  12096  neipsm  12218  cnf  12268  cnima  12284  txdis1cn  12342  hmeocnvcn  12370  psmetxrge0  12396  isxmet2d  12412  xmstopn  12519  mstopn  12520  bdxmet  12565  divcnap  12619  ivthinclemlr  12679  ivthinclemur  12681  dvlemap  12713  dvcnp2cntop  12727  dvaddxxbr  12729  dvmulxxbr  12730  dvcoapbr  12735  dvcjbr  12736  dvrecap  12741  dveflem  12750  bj-indsuc  12949  nnsf  13022  nninfalllemn  13025
  Copyright terms: Public domain W3C validator