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 1005 | 1 ⊢ (𝜑 → 𝜒) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ↔ wb 104 ∧ w3a 973 |
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 975 |
This theorem is referenced by: 0ellim 4383 smodm 6270 erdm 6523 ixpfn 6682 dif1en 6857 eluzelz 9496 elfz3nn0 10071 ef01bndlem 11719 sin01bnd 11720 cos01bnd 11721 sin01gt0 11724 gznegcl 12327 gzcjcl 12328 gzaddcl 12329 gzmulcl 12330 gzabssqcl 12333 4sqlem4a 12343 reeff1oleme 13487 cosq14gt0 13547 cosq23lt0 13548 coseq0q4123 13549 coseq00topi 13550 coseq0negpitopi 13551 cosq34lt1 13565 cos02pilt1 13566 ioocosf1o 13569 2sqlem2 13745 2sqlem3 13747 |
Copyright terms: Public domain | W3C validator |