![]() |
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 429 | 1 ⊢ (𝜑 → (𝜒 → 𝜃)) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ wa 104 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 |
This theorem depends on definitions: df-bi 117 |
This theorem is referenced by: mp2ani 432 mulgt1 8850 recgt1i 8885 recreclt 8887 nngt0 8974 nnrecgt0 8987 elnnnn0c 9251 elnnz1 9306 recnz 9376 uz3m2nn 9603 ledivge1le 9756 expubnd 10608 expnbnd 10675 expnlbnd 10676 sin02gt0 11803 oddge22np1 11918 dvdsnprmd 12157 reeff1olem 14649 sinq12gt0 14708 logdivlti 14759 |
Copyright terms: Public domain | W3C validator |