Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > mpani | Structured version Visualization version GIF 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 691 | 1 ⊢ (𝜑 → (𝜒 → 𝜃)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 396 |
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 208 df-an 397 |
This theorem is referenced by: mp2ani 694 wfi 6174 ordelinel 6282 dif20el 8119 domunfican 8779 mulgt1 11487 recgt1i 11525 recreclt 11527 ledivp1i 11553 nngt0 11656 nnrecgt0 11668 elnnnn0c 11930 elnnz1 11996 recnz 12045 uz3m2nn 12279 ledivge1le 12448 xrub 12693 1mod 13259 expubnd 13529 expnbnd 13581 expnlbnd 13582 hashgt23el 13773 resqrex 14598 sin02gt0 15533 oddge22np1 15686 dvdsnprmd 16022 prmlem1 16429 prmlem2 16441 lsmss2 18722 ovolicopnf 24052 voliunlem3 24080 volsup 24084 volivth 24135 itg2seq 24270 itg2monolem2 24279 reeff1olem 24961 sinq12gt0 25020 logdivlti 25130 logdivlt 25131 efexple 25784 gausslemma2dlem4 25872 axlowdimlem16 26670 axlowdimlem17 26671 axlowdim 26674 rusgr1vtx 27297 dmdbr2 30007 dfon2lem3 32927 dfon2lem7 32931 frpoind 32977 frind 32982 nn0prpwlem 33567 bj-resta 34281 tan2h 34765 mblfinlem4 34813 m1mod0mod1 43406 iccpartgt 43464 gbegt5 43803 gbowgt5 43804 sbgoldbalt 43823 sgoldbeven3prm 43825 nnsum4primesodd 43838 nnsum4primesoddALTV 43839 evengpoap3 43841 nnsum4primesevenALTV 43843 m1modmmod 44509 difmodm1lt 44510 regt1loggt0 44524 rege1logbrege0 44546 rege1logbzge0 44547 |
Copyright terms: Public domain | W3C validator |