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 ⊢ ((𝜑 → 𝜓) → 𝜒)

This proof depends on syntax axioms:  ¬ wn 3   → wi 4

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem is used by:  jad  189  pm2.01  190  peirce  205  oibabs  966  pm2.74  990  pm5.71  1045  meredith  1674  tbw-bijust  1731  tbw-negdf  1732  merco1  1746  19.38  1872  19.35  1910  sbrimvw  2128  sbi2  2339  dfmoeu  2565  moabs  2573  exmoeu  2611  moanimlem  2648  r19.35  3125  r19.21v  3192  elab3gf  3645  elab3g  3646  dfss2  3924  r19.2zb  4463  ralidmw  4479  ralidm  4480  iununi  5067  asymref2  6119  nelaneqOLDOLD  9573  fsuppmapnn0fiub0  14049  itgeq2  25990  frgrwopreglem4a  30734  meran1  36981  imsym1  36988  bj-cbvaw  37322  bj-cbveaw  37324  bj-ssbid2ALT  37344  wl-moteq  38228  axc5c7  39745  axc5c711  39752  eu6w  43468  rp-fakeimass  44298  nanorxor  45075  axc5c4c711  45171  pm2.43cbi  45287  euoreqb  47906  oppcendc  49855