Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > mpani | Structured version Visualization 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 711 | 1 |
Colors of variables: wff setvar class |
Syntax hints: wi 4 wa 384 |
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 197 df-an 386 |
This theorem is referenced by: mp2ani 714 wfi 5713 ordelinel 5825 ordelinelOLD 5826 dif20el 7585 domunfican 8233 mulgt1 10882 recgt1i 10920 recreclt 10922 ledivp1i 10949 nngt0 11049 nnrecgt0 11058 elnnnn0c 11338 elnnz1 11403 recnz 11452 uz3m2nn 11731 ledivge1le 11901 xrub 12142 1mod 12702 expubnd 12921 expnbnd 12993 expnlbnd 12994 resqrex 13991 sin02gt0 14922 oddge22np1 15073 dvdsnprmd 15403 prmlem1 15814 prmlem2 15827 lsmss2 18081 ovolicopnf 23292 voliunlem3 23320 volsup 23324 volivth 23375 itg2seq 23509 itg2monolem2 23518 reeff1olem 24200 sinq12gt0 24259 logdivlti 24366 logdivlt 24367 efexple 25006 gausslemma2dlem4 25094 axlowdimlem16 25837 axlowdimlem17 25838 axlowdim 25841 rusgr1vtx 26484 dmdbr2 29162 dfon2lem3 31690 dfon2lem7 31694 frind 31740 nn0prpwlem 32317 bj-resta 33049 tan2h 33401 mblfinlem4 33449 m1mod0mod1 41339 iccpartgt 41363 pfx2 41412 gbegt5 41649 gbowgt5 41650 sbgoldbalt 41669 sgoldbeven3prm 41671 nnsum4primesodd 41684 nnsum4primesoddALTV 41685 evengpoap3 41687 nnsum4primesevenALTV 41689 m1modmmod 42316 difmodm1lt 42317 regt1loggt0 42330 rege1logbrege0 42352 rege1logbzge0 42353 |
Copyright terms: Public domain | W3C validator |