![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > mpanl1 | Unicode version |
Description: An inference based on modus ponens. (Contributed by NM, 16-Aug-1994.) (Proof shortened by Wolf Lammen, 7-Apr-2013.) |
Ref | Expression |
---|---|
mpanl1.1 |
![]() ![]() |
mpanl1.2 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
mpanl1 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | mpanl1.1 |
. . 3
![]() ![]() | |
2 | 1 | jctl 314 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
3 | mpanl1.2 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
4 | 2, 3 | sylan 283 |
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-ia1 106 ax-ia2 107 ax-ia3 108 |
This theorem is referenced by: mpanl12 436 ercnv 6550 rec11api 8696 divdiv23apzi 8708 recp1lt1 8842 divgt0i 8853 divge0i 8854 ltreci 8855 lereci 8856 lt2msqi 8857 le2msqi 8858 msq11i 8859 ltdiv23i 8869 fnn0ind 9355 elfzp1b 10080 elfzm1b 10081 sqrt11i 11122 sqrtmuli 11123 sqrtmsq2i 11125 sqrtlei 11126 sqrtlti 11127 |
Copyright terms: Public domain | W3C validator |