![]() |
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 674 | 1 ⊢ (𝜑 → (𝜓 → 𝜃)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 382 |
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 197 df-an 383 |
This theorem is referenced by: tcwf 8910 cflecard 9277 sqrlem7 14193 setciso 16944 lsmss1 18282 sincosq1lem 24466 pjcompi 28867 mdsl1i 29516 dfon2lem3 32022 dfon2lem7 32026 tan2h 33730 dvasin 33824 ismrc 37787 nnsum4primes4 42202 nnsum4primesprm 42204 nnsum4primesgbe 42206 nnsum4primesle9 42208 rngciso 42507 rngcisoALTV 42519 ringciso 42558 ringcisoALTV 42582 aacllem 43075 |
Copyright terms: Public domain | W3C validator |