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 124 pm3.2i 266 sstri 3008 0disj 3782 disjx0 3784 ontr2exmid 4268 0elsucexmid 4308 relres 4657 cnvdif 4750 funopab4 4957 fun0 4977 fvsn 5379 reltpos 5888 tpostpos 5902 tpos0 5912 swoer 6157 xpiderm 6200 erinxp 6203 domfiexmid 6363 diffitest 6371 ltrel 7174 lerel 7176 frecfzennn 9419 |
Copyright terms: Public domain | W3C validator |