![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > anim1i | GIF version |
Description: Introduce conjunct to both sides of an implication. (Contributed by NM, 5-Aug-1993.) |
Ref | Expression |
---|---|
anim1i.1 | ⊢ (φ → ψ) |
Ref | Expression |
---|---|
anim1i | ⊢ ((φ ∧ χ) → (ψ ∧ χ)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | anim1i.1 | . 2 ⊢ (φ → ψ) | |
2 | id 19 | . 2 ⊢ (χ → χ) | |
3 | 1, 2 | anim12i 321 | 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 is referenced by: sylanl1 382 sylanr1 384 mpan10 443 sbcof2 1688 sbidm 1728 disamis 2008 fun11uni 4912 fabexg 5020 fores 5058 f1oabexg 5081 fun11iun 5090 fvelrnb 5164 ssimaex 5177 foeqcnvco 5373 f1eqcocnv 5374 isoini 5400 brtposg 5810 elni2 6298 dmaddpqlem 6361 nqpi 6362 ltexnqq 6391 nq0nn 6425 nqnq0a 6437 nqnq0m 6438 elnp1st2nd 6459 mullocprlem 6551 cnegexlem3 6985 lediv2a 7642 btwnz 8133 eluz2b2 8316 uz2mulcl 8321 eqreznegel 8325 elioo4g 8573 fz0fzelfz0 8754 fz0fzdiffz0 8757 2ffzeq 8768 elfzodifsumelfzo 8827 elfzom1elp1fzo 8828 zpnn0elfzo 8833 expcl2lemap 8921 mulreap 9092 redivap 9102 imdivap 9109 |
Copyright terms: Public domain | W3C validator |