| Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > mpan2i | Structured version Visualization version GIF version | ||
| Description: An inference based on modus ponens. (Contributed by NM, 10-Apr-1994.) (Proof shortened by Wolf Lammen, 19-Nov-2012.) |
| Ref | Expression |
|---|---|
| mpan2i.1 | ⊢ 𝜒 |
| mpan2i.2 | ⊢ (𝜑 → ((𝜓 ∧ 𝜒) → 𝜃)) |
| Ref | Expression |
|---|---|
| mpan2i | ⊢ (𝜑 → (𝜓 → 𝜃)) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | mpan2i.1 | . . 3 ⊢ 𝜒 | |
| 2 | 1 | a1i 11 | . 2 ⊢ (𝜑 → 𝜒) |
| 3 | mpan2i.2 | . 2 ⊢ (𝜑 → ((𝜓 ∧ 𝜒) → 𝜃)) | |
| 4 | 2, 3 | mpan2d 694 | 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: tcwf 9923 cflecard 10293 01sqrexlem7 15287 setciso 18136 lsmss1 19683 rngciso 20638 ringciso 20672 sincosq1lem 26539 pjcompi 31691 mdsl1i 32340 dfon2lem3 35786 dfon2lem7 35790 tan2h 37619 dvasin 37711 ismrc 42712 nnsum4primes4 47776 nnsum4primesprm 47778 nnsum4primesgbe 47780 nnsum4primesle9 47782 rngcisoALTV 48193 ringcisoALTV 48227 aacllem 49320 |
| Copyright terms: Public domain | W3C validator |