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  2335  dfmoeu  2560  moabs  2568  exmoeu  2606  moanimlem  2643  r19.35  3120  r19.21v  3187  elab3gf  3638  elab3g  3639  dfss2  3917  r19.2zb  4456  ralidmw  4472  ralidm  4473  iununi  5059  asymref2  6111  nelaneqOLDOLD  9577  fsuppmapnn0fiub0  14058  itgeq2  26006  frgrwopreglem4a  30791  meran1  37031  imsym1  37038  bj-cbvaw  37372  bj-cbveaw  37374  bj-ssbid2ALT  37394  wl-moteq  38278  axc5c7  39785  axc5c711  39792  eu6w  43523  rp-fakeimass  44353  nanorxor  45130  axc5c4c711  45226  pm2.43cbi  45342  euoreqb  47998  oppcendc  49945