![]() |
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 318 | 1 ⊢ (φ → ((θ ∧ ψ) → (θ ∧ χ))) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ wa 97 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 99 ax-ia2 100 ax-ia3 101 |
This theorem depends on definitions: df-bi 110 |
This theorem is referenced by: spsbim 1721 ssel 2933 sscon 3071 uniss 3592 trel3 3853 copsexg 3972 ssopab2 4003 coss1 4434 fununi 4910 imadif 4922 fss 4997 ssimaex 5177 opabbrex 5491 ssoprab2 5503 poxp 5794 xpdom2 6241 |
Copyright terms: Public domain | W3C validator |