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

Theorem simplbi 263
 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 117 . 2 (𝜑 → (𝜓𝜒))
32simpld 109 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 This theorem depends on definitions:  df-bi 114 This theorem is referenced by:  pm5.62dc  863  3simpa  912  xoror  1286  anxordi  1307  sbidm  1747  reurex  2540  eqimss  3025  pssss  3067  eldifi  3094  inss1  3185  sopo  4078  wefr  4123  ordtr  4143  opelxp1  4405  relop  4514  funmo  4945  funrel  4947  fnfun  5024  ffn  5074  f1f  5120  f1of1  5153  f1ofo  5161  isof1o  5475  eqopi  5826  1st2nd2  5829  reldmtpos  5899  swoer  6165  ecopover  6235  ecopoverg  6238  dfplpq2  6510  enq0ref  6589  cauappcvgprlemopl  6802  cauappcvgprlemdisj  6807  caucvgprlemopl  6825  caucvgprlemdisj  6830  caucvgprprlemopl  6853  caucvgprprlemopu  6855  caucvgprprlemdisj  6858  peano1nnnn  6986  axrnegex  7011  ltxrlt  7144  1nn  8001  zre  8306  nnssz  8319  ixxss1  8874  ixxss2  8875  ixxss12  8876  iccss2  8914  rge0ssre  8947  elfzuz  8988  uzdisj  9057  nn0disj  9097  frecuzrdgfn  9362  oddpwdc  10262  bj-indint  10442  bj-inf2vnlem2  10483
 Copyright terms: Public domain W3C validator