|   | 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 524 | . 2 ⊢ (𝜑 → (𝜑 ∧ 𝜓)) | 
| 3 | mpanl2.2 | . 2 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃) | |
| 4 | 2, 3 | sylan 580 | 1 ⊢ ((𝜑 ∧ 𝜒) → 𝜃) | 
| Colors of variables: wff setvar class | 
| Syntax hints: → wi 4 ∧ wa 395 | 
| 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 207 df-an 396 | 
| This theorem is referenced by: mpanr1 703 mp3an2 1450 reuss 4326 tfrlem11 8429 tfr3 8440 oe0 8561 unfi 9212 dif1ennnALT 9312 indpi 10948 map2psrpr 11151 axcnre 11205 muleqadd 11908 divdiv2 11980 addltmul 12504 supxrpnf 13361 supxrunb1 13362 supxrunb2 13363 iimulcl 24967 clwwlknonex2lem2 30128 nmopadjlem 32109 nmopcoadji 32121 opsqrlem6 32165 hstrbi 32286 sgncl 34542 poimirlem3 37631 dflim5 43347 aacllem 49375 | 
| Copyright terms: Public domain | W3C validator |