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  202  oibabs  953  pm2.74  976  pm5.71  1029  meredith  1641  tbw-bijust  1698  tbw-negdf  1699  merco1  1713  19.38  1839  19.35  1877  sbi2  2302  dfmoeu  2535  moabs  2542  exmoeu  2580  moanimlem  2617  r19.35  3095  r19.35OLD  3096  r19.21v  3165  elab3gf  3663  elab3g  3664  dfss2  3944  r19.2zb  4471  ralidmw  4483  ralidm  4487  iununi  5075  asymref2  6106  nelaneq  9613  fsuppmapnn0fiub0  14011  itgeq2  25731  frgrwopreglem4a  30291  meran1  36429  imsym1  36436  bj-ssbid2ALT  36681  wl-moteq  37532  axc5c7  38929  axc5c711  38936  eu6w  42699  rp-fakeimass  43536  nanorxor  44329  axc5c4c711  44425  pm2.43cbi  44543  euoreqb  47138  oppcendc  48993