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 979 | 1 ⊢ (𝜑 → 𝜒) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ↔ wb 104 ∧ w3a 947 |
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 949 |
This theorem is referenced by: 0ellim 4290 smodm 6156 erdm 6407 ixpfn 6566 dif1en 6741 eluzelz 9303 elfz3nn0 9863 ef01bndlem 11390 sin01bnd 11391 cos01bnd 11392 sin01gt0 11395 cosq14gt0 12840 cosq23lt0 12841 coseq0q4123 12842 coseq00topi 12843 coseq0negpitopi 12844 cosq34lt1 12858 cos02pilt1 12859 |
Copyright terms: Public domain | W3C validator |