![]() |
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-1 5 ax-2 6 ax-mp 7 |
This theorem is referenced by: imim12i 59 imim3i 61 imim21b 251 jcab 571 pm3.48 735 con1dc 792 jadc 799 pm4.78i 847 pm5.6r 875 exbir 1371 19.21h 1495 nford 1505 19.21ht 1519 exim 1536 i19.24 1576 equsexd 1665 equvini 1689 nfexd 1692 sbimi 1695 sbcof2 1739 nfsb2or 1766 mopick 2027 r19.32r 2517 r19.36av 2521 ceqsalt 2648 vtoclgft 2672 spcgft 2699 spcegft 2701 elab3gf 2768 mo2icl 2797 euind 2805 reu6 2807 reuind 2823 sbciegft 2872 ssddif 3236 dfiin2g 3771 invdisj 3847 ordunisuc2r 4346 fnoprabg 5762 caucvgsr 7410 rexanre 10716 elabgft1 11982 bj-nntrans 12150 |
Copyright terms: Public domain | W3C validator |