Theorem ja 161

Description: Inference joining the antecedents of two premises. (Contributed by NM, 24-Jan-1993.) (Proof shortened by Mel L. O'Cat, 19-Feb-2008.)

Hypotheses

Ref	Expression
ja.1
ja.2

Assertion

Ref	Expression
ja

Proof of Theorem 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

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