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 333 | 1 ⊢ (𝜑 → ((𝜃 ∧ 𝜓) → (𝜃 ∧ 𝜒))) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ wa 103 |
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 |
This theorem is referenced by: spsbim 1815 ssel 3086 sscon 3205 uniss 3752 trel3 4029 copsexg 4161 ssopab2 4192 coss1 4689 fununi 5186 imadif 5198 fss 5279 ssimaex 5475 opabbrex 5808 ssoprab2 5820 poxp 6122 pmss12g 6562 ss2ixp 6598 xpdom2 6718 qbtwnxr 10028 ioc0 10033 climshftlemg 11064 bezoutlembz 11681 tgcl 12222 neipsm 12312 ssnei2 12315 tgcnp 12367 cnpnei 12377 cnptopco 12380 mopni3 12642 limcresi 12793 cnlimcim 12798 |
Copyright terms: Public domain | W3C validator |