![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > mpanr12 | Unicode version |
Description: An inference based on modus ponens. (Contributed by NM, 24-Jul-2009.) |
Ref | Expression |
---|---|
mpanr12.1 |
![]() ![]() |
mpanr12.2 |
![]() ![]() |
mpanr12.3 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
mpanr12 |
![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | mpanr12.2 |
. 2
![]() ![]() | |
2 | mpanr12.1 |
. . 3
![]() ![]() | |
3 | mpanr12.3 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
4 | 2, 3 | mpanr1 434 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
5 | 1, 4 | mpan2 422 |
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 105 ax-ia2 106 ax-ia3 107 |
This theorem is referenced by: cnvoprab 6139 2dom 6707 phplem4 6757 fiintim 6825 mulidnq 7221 nq0m0r 7288 nq0a0 7289 addpinq1 7296 0idsr 7599 1idsr 7600 00sr 7601 addresr 7669 mulresr 7670 pitonnlem2 7679 ax0id 7710 recexaplem2 8437 reclt1 8678 crap0 8740 nominpos 8981 expnass 10429 crim 10662 sqrt00 10844 mulcn2 11113 sin02gt0 11506 opoe 11628 txswaphmeo 12529 sinq34lt0t 12960 cosordlem 12978 |
Copyright terms: Public domain | W3C validator |