Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > mp4an | Unicode version |
Description: An inference based on modus ponens. (Contributed by Jeff Madsen, 15-Jun-2011.) |
Ref | Expression |
---|---|
mp4an.1 | |
mp4an.2 | |
mp4an.3 | |
mp4an.4 | |
mp4an.5 |
Ref | Expression |
---|---|
mp4an |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | mp4an.1 | . . 3 | |
2 | mp4an.2 | . . 3 | |
3 | 1, 2 | pm3.2i 257 | . 2 |
4 | mp4an.3 | . . 3 | |
5 | mp4an.4 | . . 3 | |
6 | 4, 5 | pm3.2i 257 | . 2 |
7 | mp4an.5 | . 2 | |
8 | 3, 6, 7 | mp2an 402 | 1 |
Colors of variables: wff set class |
Syntax hints: wi 4 wa 97 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia3 101 |
This theorem is referenced by: 1lt2nq 6504 m1p1sr 6845 m1m1sr 6846 0lt1sr 6850 axi2m1 6949 mul4i 7161 add4i 7176 addsub4i 7307 muladdi 7406 lt2addi 7502 le2addi 7503 mulap0i 7637 divap0i 7736 divmuldivapi 7748 divmul13api 7749 divadddivapi 7750 divdivdivapi 7751 8th4div3 8144 iap0 8148 fldiv4p1lem1div2 9147 sqrt2gt1lt2 9647 abs3lemi 9753 |
Copyright terms: Public domain | W3C validator |