![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
Mirrors > Home > MPE Home > Th. List > ja | Unicode version |
Description: Inference joining the antecedents of two premises. (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 14 | . 2 |
3 | ja.1 | . 2 | |
4 | 2, 3 | pm2.61d1 159 | 1 |
Colors of variables: wff setvar class |
Syntax hints: -. wn 3 -> wi 4 |
This theorem is referenced by: jad 162 pm2.61i 164 pm2.01 168 peirce 181 pm2.74 846 oibabs 881 pm5.71 936 dfnotOLD 1415 meredith 1472 tbw-bijust 1531 tbw-negdf 1532 merco1 1546 19.38 1662 19.35 1687 sbi2 2134 axc5c7 2241 axc5c711 2248 mo2v 2289 mo2vOLD 2290 mo2vOLDOLD 2291 exmoeu 2316 mo2OLD 2334 moanim 2350 elab3gf 3251 r19.2zb 3919 iununi 4415 asymref2 5389 fsuppmapnn0fiub0 12099 itgeq2 22184 nbcusgra 24463 wlkntrllem3 24563 frgrawopreglem4 25047 meran1 29876 imsym1 29883 amosym1 29891 wl-embant 29974 nanorxor 31185 axc5c4c711 31308 pm2.43cbi 33288 rp-fakeimass 37736 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 |
Copyright terms: Public domain | W3C validator |