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  954  pm2.74  977  pm5.71  1030  meredith  1643  tbw-bijust  1700  tbw-negdf  1701  merco1  1715  19.38  1841  19.35  1879  sbi2  2309  dfmoeu  2536  moabs  2544  exmoeu  2582  moanimlem  2619  r19.35  3096  r19.21v  3163  elab3gf  3628  elab3g  3629  dfss2  3908  r19.2zb  4441  ralidmw  4457  ralidm  4458  iununi  5042  asymref2  6075  nelaneqOLDOLD  9512  fsuppmapnn0fiub0  13949  itgeq2  25758  frgrwopreglem4a  30398  meran1  36612  imsym1  36619  bj-cbvaw  36954  bj-cbveaw  36956  bj-ssbid2ALT  36976  wl-moteq  37856  axc5c7  39374  axc5c711  39381  eu6w  43126  rp-fakeimass  43960  nanorxor  44753  axc5c4c711  44849  pm2.43cbi  44966  euoreqb  47572  oppcendc  49508