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: wi 4 |
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 2954 0disj 3761 disjx0 3763 ontr2exmid 4250 0elsucexmid 4289 relres 4639 cnvdif 4730 funopab4 4937 fun0 4957 fvsn 5358 reltpos 5865 tpostpos 5879 tpos0 5889 swoer 6134 xpiderm 6177 erinxp 6180 diffitest 6344 ltrel 7081 lerel 7083 frecfzennn 9203 |
Copyright terms: Public domain | W3C validator |