![]() |
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 53 imim3i 55 imim21b 241 jcab 535 pm3.48 698 con1dc 752 jadc 759 pm4.78i 807 pm5.6r 835 exbir 1322 19.21h 1446 nford 1456 19.21ht 1470 exim 1487 i19.24 1527 equsexd 1614 equvini 1638 nfexd 1641 sbimi 1644 sbcof2 1688 nfsb2or 1715 mopick 1975 r19.32r 2451 r19.36av 2455 ceqsalt 2574 vtoclgft 2598 spcgft 2624 spcegft 2626 elab3gf 2686 mo2icl 2714 euind 2722 reu6 2724 reuind 2738 sbciegft 2787 ssddif 3165 dfiin2g 3681 invdisj 3750 ordunisuc2r 4205 fnoprabg 5544 elabgft1 9252 bj-nntrans 9411 |
Copyright terms: Public domain | W3C validator |