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 577 jcn 626 pm4.78i 756 pm3.48 759 con1dc 826 jadc 833 pm5.6r 897 exbir 1397 19.21h 1521 nford 1531 19.21ht 1545 exim 1563 i19.24 1603 equsexd 1692 equvini 1716 nfexd 1719 sbimi 1722 sbcof2 1766 nfsb2or 1793 mopick 2055 r19.32r 2555 r19.36av 2559 ceqsalt 2686 vtoclgft 2710 spcgft 2737 spcegft 2739 elab3gf 2807 mo2icl 2836 euind 2844 reu6 2846 reuind 2862 sbciegft 2911 ssddif 3280 dfiin2g 3816 invdisj 3893 ordunisuc2r 4400 fnoprabg 5840 caucvgsr 7578 rexanre 10960 tgcnp 12305 lmcvg 12313 elabgft1 12912 bj-nntrans 13076 |
Copyright terms: Public domain | W3C validator |