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 527 | . 2 ⊢ (𝜑 → (𝜑 ∧ 𝜓)) |
3 | mpanl2.2 | . 2 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃) | |
4 | 2, 3 | sylan 582 | 1 ⊢ ((𝜑 ∧ 𝜒) → 𝜃) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 398 |
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 209 df-an 399 |
This theorem is referenced by: mpanr1 701 mp3an2 1445 reuss 4287 tfrlem11 8027 tfr3 8038 oe0 8150 dif1en 8754 indpi 10332 map2psrpr 10535 axcnre 10589 muleqadd 11287 divdiv2 11355 addltmul 11876 frnnn0supp 11956 supxrpnf 12714 supxrunb1 12715 supxrunb2 12716 iimulcl 23544 clwwlknonex2lem2 27890 nmopadjlem 29869 nmopcoadji 29881 opsqrlem6 29925 hstrbi 30046 sgncl 31800 poimirlem3 34899 aacllem 44909 |
Copyright terms: Public domain | W3C validator |