![]() |
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 526 | . 2 ⊢ (𝜑 → (𝜑 ∧ 𝜓)) |
3 | mpanl2.2 | . 2 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃) | |
4 | 2, 3 | sylan 581 | 1 ⊢ ((𝜑 ∧ 𝜒) → 𝜃) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 397 |
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 206 df-an 398 |
This theorem is referenced by: mpanr1 702 mp3an2 1450 reuss 4275 tfrlem11 8327 tfr3 8338 oe0 8461 unfi 9075 dif1ennnALT 9180 indpi 10802 map2psrpr 11005 axcnre 11059 muleqadd 11758 divdiv2 11826 addltmul 12348 supxrpnf 13192 supxrunb1 13193 supxrunb2 13194 iimulcl 24252 clwwlknonex2lem2 28881 nmopadjlem 30860 nmopcoadji 30872 opsqrlem6 30916 hstrbi 31037 sgncl 32942 poimirlem3 36013 dflim5 41564 aacllem 47143 |
Copyright terms: Public domain | W3C validator |