![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
Mirrors > Home > MPE Home > Th. List > mpani | Structured version Unicode version |
Description: An inference based on modus ponens. (Contributed by NM, 10-Apr-1994.) (Proof shortened by Wolf Lammen, 19-Nov-2012.) |
Ref | Expression |
---|---|
mpani.1 |
![]() ![]() |
mpani.2 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
mpani |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | mpani.1 |
. . 3
![]() ![]() | |
2 | 1 | a1i 11 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() |
3 | mpani.2 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
4 | 2, 3 | mpand 675 |
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 185 df-an 371 |
This theorem is referenced by: mp2ani 678 ordelinel 4924 dif20el 7054 domunfican 7694 mulgt1 10298 recgt1i 10339 recreclt 10341 ledivp1i 10368 nngt0 10461 nnrecgt0 10469 elnnnn0c 10735 elnnz1 10782 recnz 10827 xrub 11384 1mod 11856 expubnd 12040 expnbnd 12109 expnlbnd 12110 resqrex 12857 sin02gt0 13593 prmlem1 14252 prmlem2 14264 lsmss2 16285 ovolicopnf 21138 voliunlem3 21165 volsup 21169 volivth 21219 itg2seq 21352 itg2monolem2 21361 reeff1olem 22043 sinq12gt0 22101 logdivlti 22201 logdivlt 22202 efexple 22752 axlowdimlem16 23354 axlowdimlem17 23355 axlowdim 23358 dmdbr2 25858 dfon2lem3 27741 dfon2lem7 27745 wfi 27811 frind 27847 tan2h 28571 mblfinlem4 28578 nn0prpwlem 28664 uz3m2nn 30342 |
Copyright terms: Public domain | W3C validator |