Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > mp2ani | Structured version Visualization version GIF version |
Description: An inference based on modus ponens. (Contributed by NM, 12-Dec-2004.) |
Ref | Expression |
---|---|
mp2ani.1 | ⊢ 𝜓 |
mp2ani.2 | ⊢ 𝜒 |
mp2ani.3 | ⊢ (𝜑 → ((𝜓 ∧ 𝜒) → 𝜃)) |
Ref | Expression |
---|---|
mp2ani | ⊢ (𝜑 → 𝜃) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | mp2ani.2 | . 2 ⊢ 𝜒 | |
2 | mp2ani.1 | . . 3 ⊢ 𝜓 | |
3 | mp2ani.3 | . . 3 ⊢ (𝜑 → ((𝜓 ∧ 𝜒) → 𝜃)) | |
4 | 2, 3 | mpani 708 | . 2 ⊢ (𝜑 → (𝜒 → 𝜃)) |
5 | 1, 4 | mpi 20 | 1 ⊢ (𝜑 → 𝜃) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 383 |
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 196 df-an 385 |
This theorem is referenced by: dfom3 8427 dfac5lem4 8832 dfac9 8841 cflem 8951 canthp1lem2 9354 addsrpr 9775 mulsrpr 9776 trclublem 13582 gcdaddmlem 15083 sto1i 28479 stji1i 28485 kur14lem9 30450 dfon2lem4 30935 rtrclex 36943 comptiunov2i 37017 |
Copyright terms: Public domain | W3C validator |