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 706 | 1 ⊢ (𝜑 → (𝜓 → 𝜃)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 383 |
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 196 df-an 385 |
This theorem is referenced by: tcwf 8629 cflecard 8958 sqrlem7 13837 setciso 16564 lsmss1 17902 sincosq1lem 24053 pjcompi 27915 mdsl1i 28564 dfon2lem3 30934 dfon2lem7 30938 tan2h 32571 dvasin 32666 ismrc 36282 nnsum4primes4 40205 nnsum4primesprm 40207 nnsum4primesgbe 40209 nnsum4primesle9 40211 rngciso 41774 rngcisoALTV 41786 ringciso 41825 ringcisoALTV 41849 aacllem 42356 |
Copyright terms: Public domain | W3C validator |