Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE 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 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: sylanl2 383 sylanr2 385 andi 731 pm4.55dc 846 xoranor 1268 19.41h 1575 sbimi 1647 equs5e 1676 exdistrfor 1681 equs45f 1683 sbidm 1731 eu3h 1945 eupickb 1981 2exeu 1992 darii 2000 festino 2006 baroco 2007 r19.27av 2448 rspc2ev 2664 reu3 2731 sspssn 3048 difdif 3069 ssddif 3171 inssdif 3173 difin 3174 difindiss 3191 indifdir 3193 difrab 3211 iundif2ss 3722 trssord 4117 ordsuc 4287 find 4322 imainss 4739 dffun5r 4914 fof 5106 f1ocnv 5139 fv3 5197 relelfvdm 5205 funimass4 5224 fvelimab 5229 funconstss 5285 dff2 5311 dffo5 5316 dff1o6 5416 oprabid 5537 ssoprab2i 5593 releldm2 5811 recexgt0sr 6858 lediv2a 7861 elfzp12 8961 cau3lem 9710 |
Copyright terms: Public domain | W3C validator |