Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > simp3bi | GIF version |
Description: Deduce a conjunct from a triple conjunction. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) |
Ref | Expression |
---|---|
3simp1bi.1 | ⊢ (𝜑 ↔ (𝜓 ∧ 𝜒 ∧ 𝜃)) |
Ref | Expression |
---|---|
simp3bi | ⊢ (𝜑 → 𝜃) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 3simp1bi.1 | . . 3 ⊢ (𝜑 ↔ (𝜓 ∧ 𝜒 ∧ 𝜃)) | |
2 | 1 | biimpi 119 | . 2 ⊢ (𝜑 → (𝜓 ∧ 𝜒 ∧ 𝜃)) |
3 | 2 | simp3d 995 | 1 ⊢ (𝜑 → 𝜃) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ↔ wb 104 ∧ w3a 962 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 |
This theorem depends on definitions: df-bi 116 df-3an 964 |
This theorem is referenced by: limuni 4313 smores2 6184 ersym 6434 ertr 6437 fvixp 6590 fiintim 6810 eluzle 9331 ef01bndlem 11452 sin01bnd 11453 cos01bnd 11454 sin01gt0 11457 ennnfonelemim 11926 cosq14gt0 12902 cosq23lt0 12903 coseq0q4123 12904 coseq00topi 12905 coseq0negpitopi 12906 cosq34lt1 12920 cos02pilt1 12921 |
Copyright terms: Public domain | W3C validator |