![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > simp2bi | GIF version |
Description: Deduce a conjunct from a triple conjunction. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) |
Ref | Expression |
---|---|
3simp1bi.1 | ⊢ (𝜑 ↔ (𝜓 ∧ 𝜒 ∧ 𝜃)) |
Ref | Expression |
---|---|
simp2bi | ⊢ (𝜑 → 𝜒) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 3simp1bi.1 | . . 3 ⊢ (𝜑 ↔ (𝜓 ∧ 𝜒 ∧ 𝜃)) | |
2 | 1 | biimpi 119 | . 2 ⊢ (𝜑 → (𝜓 ∧ 𝜒 ∧ 𝜃)) |
3 | 2 | simp2d 995 | 1 ⊢ (𝜑 → 𝜒) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ↔ wb 104 ∧ w3a 963 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 ax-ia2 106 |
This theorem depends on definitions: df-bi 116 df-3an 965 |
This theorem is referenced by: 0ellim 4328 smodm 6196 erdm 6447 ixpfn 6606 dif1en 6781 eluzelz 9359 elfz3nn0 9926 ef01bndlem 11499 sin01bnd 11500 cos01bnd 11501 sin01gt0 11504 reeff1oleme 12901 cosq14gt0 12961 cosq23lt0 12962 coseq0q4123 12963 coseq00topi 12964 coseq0negpitopi 12965 cosq34lt1 12979 cos02pilt1 12980 ioocosf1o 12983 |
Copyright terms: Public domain | W3C validator |