New Foundations Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > NFE Home > Th. List > anim2i | GIF version |
Description: Introduce conjunct to both sides of an implication. (Contributed by NM, 5-Aug-1993.) |
Ref | Expression |
---|---|
anim1i.1 | ⊢ (φ → ψ) |
Ref | Expression |
---|---|
anim2i | ⊢ ((χ ∧ φ) → (χ ∧ ψ)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | id 19 | . 2 ⊢ (χ → χ) | |
2 | anim1i.1 | . 2 ⊢ (φ → ψ) | |
3 | 1, 2 | anim12i 549 | 1 ⊢ ((χ ∧ φ) → (χ ∧ ψ)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 358 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 |
This theorem depends on definitions: df-bi 177 df-an 360 |
This theorem is referenced by: sylanl2 632 sylanr2 634 andi 837 sbimi 1652 19.41 1879 ax12olem2 1928 exdistrf 1971 equs45f 1989 eupickb 2269 2eu1 2284 darii 2303 festino 2309 baroco 2310 r19.27av 2752 rspc2ev 2963 reu3 3026 difrab 3529 sfinltfin 4535 vfinspnn 4541 vinf 4555 fof 5269 fv3 5341 fvelimab 5370 fvopab4t 5385 dff2 5419 dffo5 5424 dff1o6 5475 oprabid 5550 ssoprab2i 5580 ndmovass 5618 ndmovdistr 5619 oqelins4 5794 |
Copyright terms: Public domain | W3C validator |