Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > simp1bi | GIF version |
Description: Deduce a conjunct from a triple conjunction. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) |
Ref | Expression |
---|---|
3simp1bi.1 | ⊢ (𝜑 ↔ (𝜓 ∧ 𝜒 ∧ 𝜃)) |
Ref | Expression |
---|---|
simp1bi | ⊢ (𝜑 → 𝜓) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 3simp1bi.1 | . . 3 ⊢ (𝜑 ↔ (𝜓 ∧ 𝜒 ∧ 𝜃)) | |
2 | 1 | biimpi 119 | . 2 ⊢ (𝜑 → (𝜓 ∧ 𝜒 ∧ 𝜃)) |
3 | 2 | simp1d 998 | 1 ⊢ (𝜑 → 𝜓) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ↔ wb 104 ∧ w3a 967 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 |
This theorem depends on definitions: df-bi 116 df-3an 969 |
This theorem is referenced by: limord 4367 smores2 6253 smofvon2dm 6255 smofvon 6258 errel 6501 lincmb01cmp 9930 iccf1o 9931 elfznn0 10039 elfzouz 10076 ef01bndlem 11683 sin01bnd 11684 cos01bnd 11685 sin01gt0 11688 cos01gt0 11689 sin02gt0 11690 eulerthlema 12141 modprm0 12165 coseq00topi 13303 coseq0negpitopi 13304 cosq34lt1 13318 cos11 13321 nconstwlpolemgt0 13783 |
Copyright terms: Public domain | W3C validator |