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  2530  moabs  2537  exmoeu  2575  moanimlem  2612  r19.35  3089  r19.35OLD  3090  r19.21v  3159  elab3gf  3654  elab3g  3655  dfss2  3935  r19.2zb  4462  ralidmw  4474  ralidm  4478  iununi  5066  asymref2  6093  nelaneq  9559  fsuppmapnn0fiub0  13965  itgeq2  25686  frgrwopreglem4a  30246  meran1  36406  imsym1  36413  bj-ssbid2ALT  36658  wl-moteq  37509  axc5c7  38911  axc5c711  38918  eu6w  42671  rp-fakeimass  43508  nanorxor  44301  axc5c4c711  44397  pm2.43cbi  44515  euoreqb  47114  oppcendc  49011