![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > mpani | 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 9 | . 2 ⊢ (𝜑 → 𝜓) |
3 | mpani.2 | . 2 ⊢ (𝜑 → ((𝜓 ∧ 𝜒) → 𝜃)) | |
4 | 2, 3 | mpand 426 | 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 depends on definitions: df-bi 116 |
This theorem is referenced by: mp2ani 429 mulgt1 8645 recgt1i 8680 recreclt 8682 nngt0 8769 nnrecgt0 8782 elnnnn0c 9046 elnnz1 9101 recnz 9168 uz3m2nn 9395 ledivge1le 9543 expubnd 10381 expnbnd 10446 expnlbnd 10447 sin02gt0 11506 oddge22np1 11614 dvdsnprmd 11842 reeff1olem 12900 sinq12gt0 12959 logdivlti 13010 |
Copyright terms: Public domain | W3C validator |