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

Theorem simplbi 269
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-1 5  ax-2 6  ax-mp 7  ax-ia1 105
This theorem depends on definitions:  df-bi 116
This theorem is referenced by:  pm5.62dc  892  3simpa  941  xoror  1316  anxordi  1337  sbidm  1780  reurex  2581  eqimss  3079  eldifi  3123  elinel1  3187  inss1  3221  sopo  4149  wefr  4194  ordtr  4214  opelxp1  4485  relop  4599  funmo  5043  funrel  5045  funinsn  5076  fnfun  5124  ffn  5174  f1f  5229  f1of1  5265  f1ofo  5273  isof1o  5600  eqopi  5956  1st2nd2  5959  reldmtpos  6032  swoer  6334  ecopover  6404  ecopoverg  6407  fnfi  6700  casef  6833  dfplpq2  6974  enq0ref  7053  cauappcvgprlemopl  7266  cauappcvgprlemdisj  7271  caucvgprlemopl  7289  caucvgprlemdisj  7294  caucvgprprlemopl  7317  caucvgprprlemopu  7319  caucvgprprlemdisj  7322  peano1nnnn  7450  axrnegex  7475  ltxrlt  7613  1nn  8494  zre  8815  nnssz  8828  ixxss1  9383  ixxss2  9384  ixxss12  9385  iccss2  9423  rge0ssre  9456  elfzuz  9497  uzdisj  9568  nn0disj  9610  frecuzrdgtcl  9880  frecuzrdgfunlem  9887  modfsummodlemstep  10912  mertenslem2  10991  prmnn  11431  prmuz2  11451  oddpwdc  11491  sqpweven  11492  2sqpwodd  11493  phimullem  11540  hashgcdlem  11542  topontop  11774  tpstop  11794  bj-indint  12099  bj-inf2vnlem2  12139  nninff  12166  peano4nninf  12168
  Copyright terms: Public domain W3C validator