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  2535  moabs  2543  exmoeu  2581  moanimlem  2618  r19.35  3095  r19.21v  3162  elab3gf  3627  elab3g  3628  dfss2  3907  r19.2zb  4440  ralidmw  4456  ralidm  4457  iununi  5041  asymref2  6080  nelaneqOLDOLD  9518  fsuppmapnn0fiub0  13955  itgeq2  25745  frgrwopreglem4a  30380  meran1  36593  imsym1  36600  bj-cbvaw  36935  bj-cbveaw  36937  bj-ssbid2ALT  36957  wl-moteq  37839  axc5c7  39357  axc5c711  39364  eu6w  43109  rp-fakeimass  43939  nanorxor  44732  axc5c4c711  44828  pm2.43cbi  44945  euoreqb  47557  oppcendc  49493