![]() |
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 201 oibabs 950 pm2.74 973 pm5.71 1026 meredith 1643 tbw-bijust 1700 tbw-negdf 1701 merco1 1715 19.38 1841 19.35 1880 sbi2 2298 dfmoeu 2530 moabs 2537 exmoeu 2575 moanimlem 2614 r19.35 3108 r19.35OLD 3109 r19.21v 3179 elab3gf 3674 elab3g 3675 r19.2zb 4495 ralidmw 4507 ralidm 4511 iununi 5102 asymref2 6118 nelaneq 9596 fsuppmapnn0fiub0 13960 itgeq2 25302 frgrwopreglem4a 29601 meran1 35388 imsym1 35395 bj-ssbid2ALT 35632 wl-moteq 36475 axc5c7 37873 axc5c711 37880 rp-fakeimass 42351 nanorxor 43152 axc5c4c711 43248 pm2.43cbi 43367 euoreqb 45902 |
Copyright terms: Public domain | W3C validator |