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  2336  dfmoeu  2561  moabs  2569  exmoeu  2607  moanimlem  2644  r19.35  3121  r19.21v  3188  elab3gf  3638  elab3g  3639  dfss2  3917  r19.2zb  4456  ralidmw  4472  ralidm  4473  iununi  5059  asymref2  6111  nelaneqOLDOLD  9598  fsuppmapnn0fiub0  14136  itgeq2  26098  frgrwopreglem4a  30911  meran1  37199  imsym1  37206  bj-cbvaw  37540  bj-cbveaw  37542  bj-ssbid2ALT  37562  wl-moteq  38446  axc5c7  39968  axc5c711  39975  eu6w  43687  rp-fakeimass  44512  nanorxor  45288  axc5c4c711  45384  pm2.43cbi  45500  euoreqb  48178  oppcendc  50125