![]() |
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 949 pm2.74 972 pm5.71 1025 meredith 1642 tbw-bijust 1699 tbw-negdf 1700 merco1 1714 19.38 1840 19.35 1879 sbi2 2297 dfmoeu 2529 moabs 2536 exmoeu 2574 moanimlem 2613 r19.35 3107 r19.35OLD 3108 r19.21v 3178 elab3gf 3674 elab3g 3675 r19.2zb 4495 ralidmw 4507 ralidm 4511 iununi 5102 asymref2 6118 nelaneq 9600 fsuppmapnn0fiub0 13965 itgeq2 25627 frgrwopreglem4a 29996 meran1 35760 imsym1 35767 bj-ssbid2ALT 36004 wl-moteq 36847 axc5c7 38245 axc5c711 38252 rp-fakeimass 42726 nanorxor 43527 axc5c4c711 43623 pm2.43cbi 43742 euoreqb 46276 |
Copyright terms: Public domain | W3C validator |