![]() |
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 272 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() |
4 | mp4an.3 |
. . 3
![]() ![]() | |
5 | mp4an.4 |
. . 3
![]() ![]() | |
6 | 4, 5 | pm3.2i 272 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() |
7 | mp4an.5 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
8 | 3, 6, 7 | mp2an 426 |
1
![]() ![]() |
Colors of variables: wff set class |
Syntax hints: ![]() ![]() |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia3 108 |
This theorem is referenced by: 1lt2nq 7404 m1p1sr 7758 m1m1sr 7759 0lt1sr 7763 axi2m1 7873 mul4i 8104 add4i 8121 addsub4i 8252 muladdi 8365 lt2addi 8466 le2addi 8467 mulap0i 8612 divap0i 8716 divmuldivapi 8728 divmul13api 8729 divadddivapi 8730 divdivdivapi 8731 subrecapi 8796 8th4div3 9137 iap0 9141 fldiv4p1lem1div2 10304 sqrt2gt1lt2 11057 abs3lemi 11165 3dvds2dec 11870 flodddiv4 11938 nprmi 12123 sinhalfpilem 14182 cos0pilt1 14243 lgsdir2lem1 14399 lgsdir2lem5 14403 m1lgs 14422 |
Copyright terms: Public domain | W3C validator |