Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > imim2i | Unicode version |
Description: Inference adding common antecedents in an implication. (Contributed by NM, 5-Aug-1993.) |
Ref | Expression |
---|---|
imim2i.1 |
Ref | Expression |
---|---|
imim2i |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | imim2i.1 | . . 3 | |
2 | 1 | a1i 9 | . 2 |
3 | 2 | a2i 11 | 1 |
Colors of variables: wff set class |
Syntax hints: wi 4 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 |
This theorem is referenced by: imim12i 59 imim3i 61 imim21b 251 jcab 598 pm4.78i 777 pm3.48 780 con1dc 851 jadc 858 pm5.6r 922 exbir 1429 19.21h 1550 nford 1560 19.21ht 1574 exim 1592 i19.24 1632 equsexd 1722 equvini 1751 nfexd 1754 sbimi 1757 sbcof2 1803 nfsb2or 1830 mopick 2097 r19.32r 2616 r19.36av 2621 ceqsalt 2756 vtoclgft 2780 spcgft 2807 spcegft 2809 elab3gf 2880 mo2icl 2909 euind 2917 reu6 2919 reuind 2935 sbciegft 2985 ssddif 3361 dfiin2g 3904 invdisj 3981 ordunisuc2r 4496 fnoprabg 5952 caucvgsr 7757 rexanre 11177 tgcnp 12968 lmcvg 12976 elabgft1 13778 bj-nntrans 13951 |
Copyright terms: Public domain | W3C validator |