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  1912  sbrimvw  2130  sbi2  2339  dfmoeu  2563  moabs  2571  exmoeu  2609  moanimlem  2646  r19.35  3124  r19.21v  3191  elab3gf  3641  elab3g  3642  dfss2  4097  r19.2zb  4459  ralidmw  4475  ralidm  4476  iununi  5064  asymref2  6129  nelaneqOLDOLD  9635  fsuppmapnn0fiub0  14176  itgeq2  26153  frgrwopreglem4a  30968  rmo6  35821  meran1  37414  imsym1  37421  bj-cbvaw  37755  bj-cbveaw  37757  bj-ssbid2ALT  37777  wl-moteq  38714  axc5c7  40234  axc5c711  40241  eu6w  43953  rp-fakeimass  44774  nanorxor  45550  axc5c4c711  45646  pm2.43cbi  45761  euoreqb  48453  oppcendc  50463