Theorem ja 175

Description: Inference joining the antecedents of two premises. For partial converses, see jarri 107 and jarli 124. (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 16	. 2 ⊢ ((𝜑 → 𝜓) → (𝜑 → 𝜒))
3		ja.1	. 2 ⊢ (¬ 𝜑 → 𝜒)
4	2, 3	pm2.61d1 173	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  176  pm2.61i  177  pm2.01  181  peirce  194  oibabs  937  pm2.74  960  pm5.71  1013  meredith  1685  tbw-bijust  1742  tbw-negdf  1743  merco1  1757  19.38  1882  19.35  1924  sbi2v  2279  sbi2  2469  moabs  2555  exmoeu  2601  dfmo  2615  exmoeuOLD  2632  moanimlem  2653  elab3gf  3564  r19.2zb  4284  iununi  4846  asymref2  5770  nelaneq  8795  fsuppmapnn0fiub0  13116  itgeq2  23992  frgrwopreglem4a  27735  meran1  33001  imsym1  33008  amosym1  33016  bj-ssbid2ALT  33244  wl-moteq  33899  axc5c7  35074  axc5c711  35081  rp-fakeimass  38829  nanorxor  39474  axc5c4c711  39571  pm2.43cbi  39692  euoreqb  42155