Theorem ja 188

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

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 182	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  189  pm2.61iOLD  190  pm2.01  191  peirce  204  oibabs  948  pm2.74  971  pm5.71  1024  meredith  1642  tbw-bijust  1699  tbw-negdf  1700  merco1  1714  19.38  1839  19.35  1878  sbi2  2310  sbi2vOLD  2324  sbi2ALT  2607  dfmoeu  2618  moabs  2625  exmoeu  2666  moanimlem  2703  r19.35  3341  elab3gf  3672  r19.2zb  4441  iununi  5021  asymref2  5977  nelaneq  9063  fsuppmapnn0fiub0  13362  itgeq2  24378  frgrwopreglem4a  28089  meran1  33759  imsym1  33766  amosym1  33774  bj-ssbid2ALT  33996  wl-moteq  34769  axc5c7  36062  axc5c711  36069  rp-fakeimass  39898  nanorxor  40657  axc5c4c711  40753  pm2.43cbi  40872  euoreqb  43328