![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > mpanr1 | Structured version Visualization version Unicode version |
Description: An inference based on modus ponens. (Contributed by NM, 3-May-1994.) (Proof shortened by Andrew Salmon, 7-May-2011.) |
Ref | Expression |
---|---|
mpanr1.1 |
![]() ![]() |
mpanr1.2 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
mpanr1 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | mpanr1.1 |
. 2
![]() ![]() | |
2 | mpanr1.2 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
3 | 2 | anassrs 658 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
4 | 1, 3 | mpanl2 692 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff setvar class |
Syntax hints: ![]() ![]() |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 |
This theorem depends on definitions: df-bi 190 df-an 377 |
This theorem is referenced by: mpanr12 696 oacl 7262 omcl 7263 oaordi 7272 oawordri 7276 oaass 7287 oarec 7288 omordi 7292 omwordri 7298 odi 7305 omass 7306 oeoelem 7324 fimax2g 7842 fimin2g 8038 axcnre 9613 divdiv23zi 10387 recp1lt1 10531 divgt0i 10542 divge0i 10543 ltreci 10544 lereci 10545 lt2msqi 10546 le2msqi 10547 msq11i 10548 ltdiv23i 10558 ltdivp1i 10560 zmin 11288 ge0gtmnf 11495 hashprg 12603 sqrt11i 13495 sqrtmuli 13496 sqrtmsq2i 13498 sqrtlei 13499 sqrtlti 13500 cos01gt0 14293 0wlk 25323 0trl 25324 0pth 25348 0spth 25349 0crct 25402 0cycl 25403 0clwlk 25541 vc2 26222 vc0 26236 vcm 26238 vcnegneg 26241 nvnncan 26332 nvpi 26343 nvge0 26351 ipval3 26393 ipidsq 26397 sspmval 26420 opsqrlem1 27841 opsqrlem6 27846 hstle 27931 hstrbi 27967 atordi 28085 poimirlem6 31990 poimirlem7 31991 poimirlem16 32000 poimirlem19 32003 poimirlem20 32004 |
Copyright terms: Public domain | W3C validator |