Theorem ja 188

Description: Inference joining the antecedents of two premises. For partial converses, see jarri 108 and jarli 127. (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 17	. 2 ⊢ ((𝜑 → 𝜓) → (𝜑 → 𝜒))
3		ja.1	. 2 ⊢ (¬ 𝜑 → 𝜒)
4	2, 3	pm2.61d1 182	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  189  pm2.01  190  peirce  205  oibabs  966  pm2.74  990  pm5.71  1045  meredith  1671  tbw-bijust  1728  tbw-negdf  1729  merco1  1743  19.38  1869  19.35  1907  sbrimvw  2125  sbi2  2337  dfmoeu  2563  moabs  2571  exmoeu  2609  moanimlem  2646  r19.35  3123  r19.21v  3190  elab3gf  3643  elab3g  3644  dfss2  3923  r19.2zb  4461  ralidmw  4477  ralidm  4478  iununi  5065  asymref2  6117  nelaneqOLDOLD  9562  fsuppmapnn0fiub0  14025  itgeq2  25937  frgrwopreglem4a  30661  meran1  36922  imsym1  36929  bj-cbvaw  37263  bj-cbveaw  37265  bj-ssbid2ALT  37285  wl-moteq  38169  axc5c7  39685  axc5c711  39692  eu6w  43408  rp-fakeimass  44238  nanorxor  45015  axc5c4c711  45111  pm2.43cbi  45227  euoreqb  47846  oppcendc  49796