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 423 | 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 7338 m1p1sr 7692 m1m1sr 7693 0lt1sr 7697 axi2m1 7807 mul4i 8037 add4i 8054 addsub4i 8185 muladdi 8298 lt2addi 8399 le2addi 8400 mulap0i 8544 divap0i 8647 divmuldivapi 8659 divmul13api 8660 divadddivapi 8661 divdivdivapi 8662 subrecapi 8727 8th4div3 9067 iap0 9071 fldiv4p1lem1div2 10230 sqrt2gt1lt2 10977 abs3lemi 11085 3dvds2dec 11788 flodddiv4 11856 nprmi 12035 sinhalfpilem 13259 cos0pilt1 13320 |
Copyright terms: Public domain | W3C validator |