![]() |
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 124. (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 173 | 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 176 pm2.61i 177 pm2.01 181 peirce 194 oibabs 937 pm2.74 960 pm5.71 1013 meredith 1685 tbw-bijust 1742 tbw-negdf 1743 merco1 1757 19.38 1882 19.35 1924 sbi2v 2279 sbi2 2469 moabs 2555 exmoeu 2601 dfmo 2615 exmoeuOLD 2632 moanimlem 2653 elab3gf 3564 r19.2zb 4284 iununi 4846 asymref2 5770 nelaneq 8795 fsuppmapnn0fiub0 13116 itgeq2 23992 frgrwopreglem4a 27735 meran1 33001 imsym1 33008 amosym1 33016 bj-ssbid2ALT 33244 wl-moteq 33899 axc5c7 35074 axc5c711 35081 rp-fakeimass 38829 nanorxor 39474 axc5c4c711 39571 pm2.43cbi 39692 euoreqb 42155 |
Copyright terms: Public domain | W3C validator |