![]() |
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 jarr 104 and jarl 174. (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 170 | 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 173 pm2.61i 175 pm2.01 179 peirce 192 pm2.74 887 oibabs 921 pm5.71 973 meredith 1557 tbw-bijust 1614 tbw-negdf 1615 merco1 1629 19.38 1757 19.35 1794 sbi2 2381 mo2v 2465 exmoeu 2490 moanim 2517 elab3gf 3325 r19.2zb 4013 iununi 4546 asymref2 5432 fsuppmapnn0fiub0 12655 itgeq2 23350 nbcusgra 25992 wlkntrllem3 26091 frgrawopreglem4 26574 meran1 31580 imsym1 31587 amosym1 31595 bj-ssbid2ALT 31835 axc5c7 33214 axc5c711 33221 rp-fakeimass 36876 nanorxor 37526 axc5c4c711 37624 pm2.43cbi 37745 frgrwopreglem4 41484 |
Copyright terms: Public domain | W3C validator |