Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > anim1i | Unicode 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 1691 sbidm 1731 disamis 2011 fun11uni 4969 fabexg 5077 fores 5115 f1oabexg 5138 fun11iun 5147 fvelrnb 5221 ssimaex 5234 foeqcnvco 5430 f1eqcocnv 5431 isoini 5457 brtposg 5869 elni2 6412 dmaddpqlem 6475 nqpi 6476 ltexnqq 6506 nq0nn 6540 nqnq0a 6552 nqnq0m 6553 elnp1st2nd 6574 mullocprlem 6668 cnegexlem3 7188 lediv2a 7861 btwnz 8357 eluz2b2 8540 uz2mulcl 8545 eqreznegel 8549 elioo4g 8803 fz0fzelfz0 8984 fz0fzdiffz0 8987 2ffzeq 8998 elfzodifsumelfzo 9057 elfzom1elp1fzo 9058 zpnn0elfzo 9063 expcl2lemap 9267 mulreap 9464 redivap 9474 imdivap 9481 caucvgrelemcau 9579 |
Copyright terms: Public domain | W3C validator |