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

Theorem simplbi 270
Description: Deduction eliminating a conjunct. (Contributed by NM, 27-May-1998.)
Hypothesis
Ref Expression
simplbi.1 (𝜑 ↔ (𝜓𝜒))
Assertion
Ref Expression
simplbi (𝜑𝜓)

Proof of Theorem simplbi
StepHypRef Expression
1 simplbi.1 . . 3 (𝜑 ↔ (𝜓𝜒))
21biimpi 119 . 2 (𝜑 → (𝜓𝜒))
32simpld 111 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
This theorem depends on definitions:  df-bi 116
This theorem is referenced by:  pm5.62dc  912  3simpa  961  xoror  1340  anxordi  1361  sbidm  1805  reurex  2619  eqimss  3119  eldifi  3166  elinel1  3230  inss1  3264  sopo  4203  wefr  4248  ordtr  4268  opelxp1  4541  relop  4657  funmo  5106  funrel  5108  funinsn  5140  fnfun  5188  ffn  5240  f1f  5296  f1of1  5332  f1ofo  5340  isof1o  5674  eqopi  6036  1st2nd2  6039  reldmtpos  6116  swoer  6423  ecopover  6493  ecopoverg  6496  fnfi  6791  casef  6939  dfplpq2  7126  enq0ref  7205  cauappcvgprlemopl  7418  cauappcvgprlemdisj  7423  caucvgprlemopl  7441  caucvgprlemdisj  7446  caucvgprprlemopl  7469  caucvgprprlemopu  7471  caucvgprprlemdisj  7474  peano1nnnn  7624  axrnegex  7651  ltxrlt  7794  1nn  8691  zre  9012  nnssz  9025  ixxss1  9638  ixxss2  9639  ixxss12  9640  iccss2  9678  rge0ssre  9711  elfzuz  9753  uzdisj  9824  nn0disj  9866  frecuzrdgtcl  10136  frecuzrdgfunlem  10143  modfsummodlemstep  11177  mertenslem2  11256  prmnn  11698  prmuz2  11718  oddpwdc  11758  sqpweven  11759  2sqpwodd  11760  phimullem  11807  hashgcdlem  11809  ctinfom  11847  ctinf  11849  topontop  12087  tpstop  12108  cntop1  12276  cntop2  12277  hmeocn  12380  isxmet2d  12423  metxmet  12430  xmstps  12532  msxms  12533  xmsxmet  12535  msmet  12536  bdxmet  12576  ivthinclemlr  12690  ivthinclemur  12692  bj-indint  12963  bj-inf2vnlem2  13003  nninff  13032  peano4nninf  13034
  Copyright terms: Public domain W3C validator