![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > mp2 | Unicode version |
Description: A double modus ponens inference. (Contributed by NM, 5-Apr-1994.) (Proof shortened by Wolf Lammen, 23-Jul-2013.) |
Ref | Expression |
---|---|
mp2.1 |
![]() ![]() |
mp2.2 |
![]() ![]() |
mp2.3 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
mp2 |
![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | mp2.1 |
. 2
![]() ![]() | |
2 | mp2.2 |
. . 3
![]() ![]() | |
3 | mp2.3 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
4 | 2, 3 | mpi 15 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() |
5 | 1, 4 | ax-mp 7 |
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: impbii 117 pm3.2i 257 sstri 2948 0disj 3752 disjx0 3754 relres 4582 cnvdif 4673 funopab4 4880 fun0 4900 fvsn 5301 reltpos 5806 tpostpos 5820 tpos0 5830 swoer 6070 xpiderm 6113 erinxp 6116 ltrel 6878 lerel 6880 frecfzennn 8884 |
Copyright terms: Public domain | W3C validator |