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  851  3simpa  900  anxordi  1288  sbidm  1728  reurex  2517  eqimss  2991  pssss  3033  eldifi  3060  inss1  3151  sopo  4041  ordtr  4081  opelxp1  4320  relop  4429  funmo  4860  funrel  4862  fnfun  4939  ffn  4989  f1f  5035  f1of1  5068  f1ofo  5076  isof1o  5390  eqopi  5740  1st2nd2  5743  reldmtpos  5809  swoer  6070  ecopover  6140  ecopoverg  6143  dfplpq2  6338  enq0ref  6415  cauappcvgprlemopl  6617  cauappcvgprlemdisj  6622  axrnegex  6743  ltxrlt  6862  1nn  7686  zre  8005  nnssz  8018  ixxss1  8523  ixxss2  8524  ixxss12  8525  iccss2  8563  rge0ssre  8596  elfzuz  8636  uzdisj  8705  nn0disj  8745  frecuzrdgfn  8859  bj-indint  9366  bj-inf2vnlem2  9401
  Copyright terms: Public domain W3C validator