![]() |
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 951 pm2.74 974 pm5.71 1027 meredith 1644 tbw-bijust 1701 tbw-negdf 1702 merco1 1716 19.38 1842 19.35 1881 sbi2 2299 dfmoeu 2535 moabs 2542 exmoeu 2580 moanimlem 2619 r19.35 3112 r19.35OLD 3113 r19.21v 3177 elab3gf 3637 elab3g 3638 r19.2zb 4454 ralidmw 4466 ralidm 4470 iununi 5060 asymref2 6072 nelaneq 9536 fsuppmapnn0fiub0 13899 itgeq2 25145 frgrwopreglem4a 29257 meran1 34886 imsym1 34893 bj-ssbid2ALT 35130 wl-moteq 35976 axc5c7 37376 axc5c711 37383 rp-fakeimass 41791 nanorxor 42592 axc5c4c711 42688 pm2.43cbi 42807 euoreqb 45348 |
Copyright terms: Public domain | W3C validator |