![]() |
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 338 | 1 ⊢ ((𝜒 ∧ 𝜑) → (𝜒 ∧ 𝜓)) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ wa 104 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 |
This theorem is referenced by: sylanl2 403 sylanr2 405 andi 818 pm4.55dc 938 xoranor 1377 19.41h 1685 sbimi 1764 equs5e 1795 exdistrfor 1800 equs45f 1802 sbidm 1851 eu3h 2071 eupickb 2107 2exeu 2118 darii 2126 festino 2132 baroco 2133 r19.27v 2604 r19.27av 2612 rspc2ev 2856 reu3 2927 difdif 3260 ssddif 3369 inssdif 3371 difin 3372 difindiss 3389 indifdir 3391 difrab 3409 iundif2ss 3952 trssord 4380 ordsuc 4562 find 4598 imainss 5044 dffun5r 5228 fof 5438 f1ocnv 5474 fv3 5538 relelfvdm 5547 funimass4 5566 fvelimab 5572 funconstss 5634 dff2 5660 dffo5 5665 dff1o6 5776 oprabid 5906 ssoprab2i 5963 releldm2 6185 ixpf 6719 recexgt0sr 7771 map2psrprg 7803 lediv2a 8850 lbreu 8900 elfzp12 10096 fihashf1rn 10763 cau3lem 11118 fsumcl2lem 11401 dvdsnegb 11810 dvds2add 11827 dvds2sub 11828 ndvdssub 11929 gcd2n0cl 11964 divgcdcoprmex 12096 cncongr1 12097 ctinfom 12423 istopfin 13391 toponcom 13418 cnptoprest 13632 |
Copyright terms: Public domain | W3C validator |