![]() |
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 251 jcab 593 pm4.78i 772 pm3.48 775 con1dc 842 jadc 849 pm5.6r 913 exbir 1413 19.21h 1537 nford 1547 19.21ht 1561 exim 1579 i19.24 1619 equsexd 1708 equvini 1732 nfexd 1735 sbimi 1738 sbcof2 1783 nfsb2or 1810 mopick 2078 r19.32r 2581 r19.36av 2585 ceqsalt 2715 vtoclgft 2739 spcgft 2766 spcegft 2768 elab3gf 2838 mo2icl 2867 euind 2875 reu6 2877 reuind 2893 sbciegft 2943 ssddif 3315 dfiin2g 3854 invdisj 3931 ordunisuc2r 4438 fnoprabg 5880 caucvgsr 7634 rexanre 11024 tgcnp 12417 lmcvg 12425 elabgft1 13156 bj-nntrans 13320 |
Copyright terms: Public domain | W3C validator |