Theorem ja 189

Description: Inference joining the antecedents of two premises. For partial converses, see jarri 107 and jarli 126. (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 183	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  190  pm2.61iOLD  191  pm2.01  192  peirce  205  oibabs  949  pm2.74  972  pm5.71  1025  meredith  1643  tbw-bijust  1700  tbw-negdf  1701  merco1  1715  19.38  1840  19.35  1878  sbi2  2306  sbi2ALT  2583  dfmoeu  2594  moabs  2601  exmoeu  2641  moanimlem  2680  r19.35  3295  elab3gf  3620  r19.2zb  4399  iununi  4984  asymref2  5944  nelaneq  9047  fsuppmapnn0fiub0  13356  itgeq2  24381  frgrwopreglem4a  28095  meran1  33872  imsym1  33879  amosym1  33887  bj-ssbid2ALT  34109  wl-moteq  34919  axc5c7  36207  axc5c711  36214  rp-fakeimass  40220  nanorxor  41009  axc5c4c711  41105  pm2.43cbi  41224  euoreqb  43665