![]() |
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 421 | 1 ⊢ (𝜑 → (𝜒 → 𝜃)) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ wa 103 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 |
This theorem depends on definitions: df-bi 116 |
This theorem is referenced by: mp2ani 424 mulgt1 8421 recgt1i 8456 recreclt 8458 nngt0 8545 nnrecgt0 8558 elnnnn0c 8816 elnnz1 8871 recnz 8938 uz3m2nn 9160 ledivge1le 9302 expubnd 10127 expnbnd 10192 expnlbnd 10193 sin02gt0 11203 oddge22np1 11308 dvdsnprmd 11534 |
Copyright terms: Public domain | W3C validator |