Theorem ja 172

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.)

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 16	. 2 ⊢ ((𝜑 → 𝜓) → (𝜑 → 𝜒))
3		ja.1	. 2 ⊢ (¬ 𝜑 → 𝜒)
4	2, 3	pm2.61d1 170	1 ⊢ ((𝜑 → 𝜓) → 𝜒)

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