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 695 | . 2 ⊢ (𝜑 → (𝜒 → 𝜃)) |
5 | 1, 4 | mpi 20 | 1 ⊢ (𝜑 → 𝜃) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 399 |
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 210 df-an 400 |
This theorem is referenced by: inf0 9068 dfom3 9094 dfac5lem4 9537 dfac9 9547 cflem 9657 canthp1lem2 10064 addsrpr 10486 mulsrpr 10487 trclublem 14346 gcdaddmlem 15862 tgjustf 26267 sto1i 30019 stji1i 30025 kur14lem9 32574 dfon2lem4 33144 rtrclex 40317 comptiunov2i 40407 |
Copyright terms: Public domain | W3C validator |