![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > mpanl2 | Structured version Visualization version GIF version |
Description: An inference based on modus ponens. (Contributed by NM, 16-Aug-1994.) (Proof shortened by Andrew Salmon, 7-May-2011.) |
Ref | Expression |
---|---|
mpanl2.1 | ⊢ 𝜓 |
mpanl2.2 | ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃) |
Ref | Expression |
---|---|
mpanl2 | ⊢ ((𝜑 ∧ 𝜒) → 𝜃) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | mpanl2.1 | . . 3 ⊢ 𝜓 | |
2 | 1 | jctr 514 | . 2 ⊢ (𝜑 → (𝜑 ∧ 𝜓)) |
3 | mpanl2.2 | . 2 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃) | |
4 | 2, 3 | sylan 569 | 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: mpanr1 683 mp3an2 1560 reuss 4056 tfrlem11 7637 tfr3 7648 oe0 7756 dif1en 8349 indpi 9931 map2psrpr 10133 axcnre 10187 muleqadd 10873 divdiv2 10939 addltmul 11470 frnnn0supp 11551 supxrpnf 12353 supxrunb1 12354 supxrunb2 12355 iimulcl 22956 clwwlknonex2lem2 27284 nmopadjlem 29288 nmopcoadji 29300 opsqrlem6 29344 hstrbi 29465 sgncl 30940 poimirlem3 33745 aacllem 43078 |
Copyright terms: Public domain | W3C validator |