![]() |
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: ![]() |
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 253 jcab 603 pm4.78i 783 pm3.48 786 con1dc 857 jadc 864 pm5.6r 928 exbir 1447 19.21h 1568 nford 1578 19.21ht 1592 exim 1610 i19.24 1650 equsexd 1740 equvini 1769 nfexd 1772 sbimi 1775 sbcof2 1821 nfsb2or 1848 mopick 2116 r19.32r 2636 r19.36av 2641 ceqsalt 2778 vtoclgft 2802 spcgft 2829 spcegft 2831 elab3gf 2902 mo2icl 2931 euind 2939 reu6 2941 reuind 2957 sbciegft 3008 ssddif 3384 dfiin2g 3934 invdisj 4012 ordunisuc2r 4531 fnoprabg 5997 caucvgsr 7831 rexanre 11261 tgcnp 14169 lmcvg 14177 elabgft1 14991 bj-nntrans 15164 |
Copyright terms: Public domain | W3C validator |