![]() |
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 120 | . 2 ⊢ (𝜑 → (𝜓 ∧ 𝜒 ∧ 𝜃)) |
3 | 2 | simp2d 1011 | 1 ⊢ (𝜑 → 𝜒) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ↔ wb 105 ∧ w3a 979 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 |
This theorem depends on definitions: df-bi 117 df-3an 981 |
This theorem is referenced by: 0ellim 4412 smodm 6309 erdm 6562 ixpfn 6721 dif1en 6896 eluzelz 9554 elfz3nn0 10132 ef01bndlem 11781 sin01bnd 11782 cos01bnd 11783 sin01gt0 11786 gznegcl 12390 gzcjcl 12391 gzaddcl 12392 gzmulcl 12393 gzabssqcl 12396 4sqlem4a 12406 xpsff1o 12790 subgss 13078 rngmgp 13250 srgmgp 13282 ringmgp 13316 lmodring 13571 lmodprop2d 13624 reeff1oleme 14576 cosq14gt0 14636 cosq23lt0 14637 coseq0q4123 14638 coseq00topi 14639 coseq0negpitopi 14640 cosq34lt1 14654 cos02pilt1 14655 ioocosf1o 14658 2sqlem2 14845 2sqlem3 14847 |
Copyright terms: Public domain | W3C validator |