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 270 | . 2 |
4 | mp4an.3 | . . 3 | |
5 | mp4an.4 | . . 3 | |
6 | 4, 5 | pm3.2i 270 | . 2 |
7 | mp4an.5 | . 2 | |
8 | 3, 6, 7 | mp2an 424 | 1 |
Colors of variables: wff set class |
Syntax hints: wi 4 wa 103 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia3 107 |
This theorem is referenced by: 1lt2nq 7355 m1p1sr 7709 m1m1sr 7710 0lt1sr 7714 axi2m1 7824 mul4i 8054 add4i 8071 addsub4i 8202 muladdi 8315 lt2addi 8416 le2addi 8417 mulap0i 8561 divap0i 8664 divmuldivapi 8676 divmul13api 8677 divadddivapi 8678 divdivdivapi 8679 subrecapi 8744 8th4div3 9084 iap0 9088 fldiv4p1lem1div2 10248 sqrt2gt1lt2 11000 abs3lemi 11108 3dvds2dec 11812 flodddiv4 11880 nprmi 12065 sinhalfpilem 13465 cos0pilt1 13526 lgsdir2lem1 13682 lgsdir2lem5 13686 |
Copyright terms: Public domain | W3C validator |