![]() |
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 7435 m1p1sr 7789 m1m1sr 7790 0lt1sr 7794 axi2m1 7904 mul4i 8135 add4i 8152 addsub4i 8283 muladdi 8396 lt2addi 8497 le2addi 8498 mulap0i 8643 divap0i 8747 divmuldivapi 8759 divmul13api 8760 divadddivapi 8761 divdivdivapi 8762 subrecapi 8827 8th4div3 9168 iap0 9172 fldiv4p1lem1div2 10336 sqrt2gt1lt2 11090 abs3lemi 11198 3dvds2dec 11903 flodddiv4 11971 nprmi 12156 sinhalfpilem 14669 cos0pilt1 14730 lgsdir2lem1 14887 lgsdir2lem5 14891 m1lgs 14910 |
Copyright terms: Public domain | W3C validator |