|   | 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 9661 dfom3 9687 dfac5lem4 10166 dfac5lem4OLD 10168 dfac9 10177 cflem 10285 cflemOLD 10286 canthp1lem2 10693 addsrpr 11115 mulsrpr 11116 trclublem 15034 gcdaddmlem 16561 tgjustf 28481 sto1i 32255 stji1i 32261 kur14lem9 35219 dfon2lem4 35787 rtrclex 43630 comptiunov2i 43719 | 
| Copyright terms: Public domain | W3C validator |