![]() |
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 266 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() |
4 | mp4an.3 |
. . 3
![]() ![]() | |
5 | mp4an.4 |
. . 3
![]() ![]() | |
6 | 4, 5 | pm3.2i 266 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() |
7 | mp4an.5 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
8 | 3, 6, 7 | mp2an 417 |
1
![]() ![]() |
Colors of variables: wff set class |
Syntax hints: ![]() ![]() |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia3 106 |
This theorem is referenced by: 1lt2nq 6963 m1p1sr 7304 m1m1sr 7305 0lt1sr 7309 axi2m1 7408 mul4i 7628 add4i 7645 addsub4i 7776 muladdi 7885 lt2addi 7986 le2addi 7987 mulap0i 8123 divap0i 8225 divmuldivapi 8237 divmul13api 8238 divadddivapi 8239 divdivdivapi 8240 8th4div3 8633 iap0 8637 fldiv4p1lem1div2 9708 sqrt2gt1lt2 10478 abs3lemi 10586 3dvds2dec 11140 flodddiv4 11208 nprmi 11380 |
Copyright terms: Public domain | W3C validator |