|   | Metamath Proof Explorer | < Previous  
      Next > Nearby theorems | |
| Mirrors > Home > MPE Home > Th. List > ja | Structured version Visualization version GIF version | ||
| Description: Inference joining the antecedents of two premises. For partial converses, see jarri 107 and jarli 126. (Contributed by NM, 24-Jan-1993.) (Proof shortened by Mel L. O'Cat, 19-Feb-2008.) | 
| Ref | Expression | 
|---|---|
| ja.1 | ⊢ (¬ 𝜑 → 𝜒) | 
| ja.2 | ⊢ (𝜓 → 𝜒) | 
| Ref | Expression | 
|---|---|
| ja | ⊢ ((𝜑 → 𝜓) → 𝜒) | 
| Step | Hyp | Ref | Expression | 
|---|---|---|---|
| 1 | ja.2 | . . 3 ⊢ (𝜓 → 𝜒) | |
| 2 | 1 | imim2i 16 | . 2 ⊢ ((𝜑 → 𝜓) → (𝜑 → 𝜒)) | 
| 3 | ja.1 | . 2 ⊢ (¬ 𝜑 → 𝜒) | |
| 4 | 2, 3 | pm2.61d1 180 | 1 ⊢ ((𝜑 → 𝜓) → 𝜒) | 
| Colors of variables: wff setvar class | 
| Syntax hints: ¬ wn 3 → wi 4 | 
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 | 
| This theorem is referenced by: jad 187 pm2.01 188 peirce 202 oibabs 954 pm2.74 977 pm5.71 1030 meredith 1641 tbw-bijust 1698 tbw-negdf 1699 merco1 1713 19.38 1839 19.35 1877 sbi2 2302 dfmoeu 2536 moabs 2543 exmoeu 2581 moanimlem 2618 r19.35 3108 r19.35OLD 3109 r19.21v 3180 elab3gf 3684 elab3g 3685 dfss2 3969 r19.2zb 4496 ralidmw 4508 ralidm 4512 iununi 5099 asymref2 6137 nelaneq 9639 fsuppmapnn0fiub0 14034 itgeq2 25813 frgrwopreglem4a 30329 meran1 36412 imsym1 36419 bj-ssbid2ALT 36664 wl-moteq 37515 axc5c7 38912 axc5c711 38919 eu6w 42686 rp-fakeimass 43525 nanorxor 44324 axc5c4c711 44420 pm2.43cbi 44538 euoreqb 47121 oppcendc 48906 | 
| Copyright terms: Public domain | W3C validator |