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

Theorem simplbi 259
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 113 . 2 (φ → (ψ χ))
32simpld 105 1 (φψ)
Colors of variables: wff set class
Syntax hints:  wi 4   wa 97  wb 98
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99
This theorem depends on definitions:  df-bi 110
This theorem is referenced by:  pm5.62dc  840  3simpa  889  anxordi  1274  sbidm  1713  reurex  2501  eqimss  2974  pssss  3016  eldifi  3043  inss1  3134  sopo  4024  ordtr  4064  opelxp1  4304  relop  4413  funmo  4843  funrel  4845  fnfun  4922  ffn  4972  f1f  5017  f1of1  5050  f1ofo  5058  isof1o  5372  eqopi  5721  1st2nd2  5724  reldmtpos  5790  swoer  6045  ecopover  6115  ecopoverg  6118  dfplpq2  6213  enq0ref  6288  axrnegex  6573  ltxrlt  6686  bj-indint  7301  bj-inf2vnlem2  7336
  Copyright terms: Public domain W3C validator