Theorem ja 186

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 180	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  187  pm2.01  188  peirce  201  oibabs  950  pm2.74  973  pm5.71  1026  meredith  1643  tbw-bijust  1700  tbw-negdf  1701  merco1  1715  19.38  1841  19.35  1880  sbi2  2298  dfmoeu  2530  moabs  2537  exmoeu  2575  moanimlem  2614  r19.35  3108  r19.35OLD  3109  r19.21v  3179  elab3gf  3674  elab3g  3675  r19.2zb  4495  ralidmw  4507  ralidm  4511  iununi  5102  asymref2  6118  nelaneq  9593  fsuppmapnn0fiub0  13957  itgeq2  25294  frgrwopreglem4a  29560  meran1  35291  imsym1  35298  bj-ssbid2ALT  35535  wl-moteq  36378  axc5c7  37776  axc5c711  37783  rp-fakeimass  42253  nanorxor  43054  axc5c4c711  43150  pm2.43cbi  43269  euoreqb  45807