![]() |
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 696 | . 2 ⊢ (𝜑 → (𝜒 → 𝜃)) |
5 | 1, 4 | mpi 20 | 1 ⊢ (𝜑 → 𝜃) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 395 |
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 207 df-an 396 |
This theorem is referenced by: inf0 9659 dfom3 9685 dfac5lem4 10164 dfac5lem4OLD 10166 dfac9 10175 cflem 10283 cflemOLD 10284 canthp1lem2 10691 addsrpr 11113 mulsrpr 11114 trclublem 15031 gcdaddmlem 16558 tgjustf 28496 sto1i 32265 stji1i 32271 kur14lem9 35199 dfon2lem4 35768 rtrclex 43607 comptiunov2i 43696 |
Copyright terms: Public domain | W3C validator |