Theorem ja 173

Description: Inference joining the antecedents of two premises. For partial converses, see jarr 106 and jarl 175. (Contributed by NM, 24-Jan-1993.) (Proof shortened by Mel L. O'Cat, 19-Feb-2008.)

Hypotheses

Ref	Expression
ja.1	|- ( -. ph -> ch )
ja.2	|- ( ps -> ch )

Assertion

Ref	Expression
ja	|- ( ( ph -> ps ) -> ch )

Proof of Theorem ja

Step	Hyp	Ref	Expression
1		ja.2	. . 3 |- ( ps -> ch )
2	1	imim2i 16	. 2 |- ( ( ph -> ps ) -> ( ph -> ch ) )
3		ja.1	. 2 |- ( -. ph -> ch )
4	2, 3	pm2.61d1 171	1 |- ( ( ph -> ps ) -> ch )

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  174  pm2.61i  176  pm2.01  180  peirce  193  pm2.74  891  oibabs  925  pm5.71  977  meredith  1566  tbw-bijust  1623  tbw-negdf  1624  merco1  1638  19.38  1766  19.35  1805  sbi2  2393  mo2v  2477  exmoeu  2502  moanim  2529  elab3gf  3356  r19.2zb  4061  iununi  4610  asymref2  5513  fsuppmapnn0fiub0  12793  itgeq2  23544  frgrwopreglem4a  27174  meran1  32410  imsym1  32417  amosym1  32425  bj-ssbid2ALT  32646  axc5c7  34196  axc5c711  34203  rp-fakeimass  37857  nanorxor  38504  axc5c4c711  38602  pm2.43cbi  38724