![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > anim2d | GIF version |
Description: Add a conjunct to left of antecedent and consequent in a deduction. (Contributed by NM, 5-Aug-1993.) |
Ref | Expression |
---|---|
anim1d.1 | ⊢ (𝜑 → (𝜓 → 𝜒)) |
Ref | Expression |
---|---|
anim2d | ⊢ (𝜑 → ((𝜃 ∧ 𝜓) → (𝜃 ∧ 𝜒))) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | idd 21 | . 2 ⊢ (𝜑 → (𝜃 → 𝜃)) | |
2 | anim1d.1 | . 2 ⊢ (𝜑 → (𝜓 → 𝜒)) | |
3 | 1, 2 | anim12d 335 | 1 ⊢ (𝜑 → ((𝜃 ∧ 𝜓) → (𝜃 ∧ 𝜒))) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ wa 104 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 |
This theorem depends on definitions: df-bi 117 |
This theorem is referenced by: spsbim 1843 ssel 3149 sscon 3269 uniss 3830 trel3 4109 copsexg 4244 ssopab2 4275 coss1 4782 fununi 5284 imadif 5296 fss 5377 ssimaex 5577 opabbrex 5918 ssoprab2 5930 poxp 6232 pmss12g 6674 ss2ixp 6710 xpdom2 6830 qbtwnxr 10255 ioc0 10260 climshftlemg 11305 bezoutlembz 11999 tgcl 13457 neipsm 13547 ssnei2 13550 tgcnp 13602 cnpnei 13612 cnptopco 13615 mopni3 13877 limcresi 14028 cnlimcim 14033 |
Copyright terms: Public domain | W3C validator |