![]() |
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 523 | . 2 ⊢ (𝜑 → (𝜑 ∧ 𝜓)) |
3 | mpanl2.2 | . 2 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃) | |
4 | 2, 3 | sylan 578 | 1 ⊢ ((𝜑 ∧ 𝜒) → 𝜃) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 394 |
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 395 |
This theorem is referenced by: mpanr1 699 mp3an2 1447 reuss 4315 tfrlem11 8390 tfr3 8401 oe0 8524 unfi 9174 dif1ennnALT 9279 indpi 10904 map2psrpr 11107 axcnre 11161 muleqadd 11862 divdiv2 11930 addltmul 12452 supxrpnf 13301 supxrunb1 13302 supxrunb2 13303 iimulcl 24680 clwwlknonex2lem2 29628 nmopadjlem 31609 nmopcoadji 31621 opsqrlem6 31665 hstrbi 31786 sgncl 33835 poimirlem3 36794 dflim5 42381 aacllem 47935 |
Copyright terms: Public domain | W3C validator |