![]() |
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 397 |
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 206 df-an 398 |
This theorem is referenced by: inf0 9612 dfom3 9638 dfac5lem4 10117 dfac9 10127 cflem 10237 canthp1lem2 10644 addsrpr 11066 mulsrpr 11067 trclublem 14938 gcdaddmlem 16461 tgjustf 27704 sto1i 31467 stji1i 31473 kur14lem9 34143 dfon2lem4 34696 rtrclex 42301 comptiunov2i 42390 |
Copyright terms: Public domain | W3C validator |