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 433 | . 2 |
5 | 1, 4 | mpan2 421 | 1 |
Colors of variables: wff set class |
Syntax hints: wi 4 wa 103 |
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 6131 2dom 6699 phplem4 6749 fiintim 6817 mulidnq 7197 nq0m0r 7264 nq0a0 7265 addpinq1 7272 0idsr 7575 1idsr 7576 00sr 7577 addresr 7645 mulresr 7646 pitonnlem2 7655 ax0id 7686 recexaplem2 8413 reclt1 8654 crap0 8716 nominpos 8957 expnass 10398 crim 10630 sqrt00 10812 mulcn2 11081 sin02gt0 11470 opoe 11592 txswaphmeo 12490 sinq34lt0t 12912 cosordlem 12930 |
Copyright terms: Public domain | W3C validator |