Theorem ja 188

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 182	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  189  pm2.61iOLD  190  pm2.01  191  peirce  204  oibabs  948  pm2.74  971  pm5.71  1024  meredith  1641  tbw-bijust  1698  tbw-negdf  1699  merco1  1713  19.38  1838  19.35  1877  sbi2  2309  sbi2vOLD  2323  sbi2ALT  2606  dfmoeu  2617  moabs  2624  exmoeu  2665  moanimlem  2702  r19.35  3344  elab3gf  3675  r19.2zb  4444  iununi  5024  asymref2  5980  nelaneq  9066  fsuppmapnn0fiub0  13364  itgeq2  24381  frgrwopreglem4a  28092  meran1  33763  imsym1  33770  amosym1  33778  bj-ssbid2ALT  34000  wl-moteq  34758  axc5c7  36051  axc5c711  36058  rp-fakeimass  39884  nanorxor  40643  axc5c4c711  40739  pm2.43cbi  40858  euoreqb  43315