Theorem ja 186

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 180	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  187  pm2.01  188  peirce  202  oibabs  953  pm2.74  976  pm5.71  1029  meredith  1641  tbw-bijust  1698  tbw-negdf  1699  merco1  1713  19.38  1839  19.35  1877  sbi2  2302  dfmoeu  2529  moabs  2536  exmoeu  2574  moanimlem  2611  r19.35  3088  r19.35OLD  3089  r19.21v  3158  elab3gf  3648  elab3g  3649  dfss2  3929  r19.2zb  4455  ralidmw  4467  ralidm  4471  iununi  5058  asymref2  6078  nelaneq  9528  fsuppmapnn0fiub0  13934  itgeq2  25655  frgrwopreglem4a  30212  meran1  36372  imsym1  36379  bj-ssbid2ALT  36624  wl-moteq  37475  axc5c7  38877  axc5c711  38884  eu6w  42637  rp-fakeimass  43474  nanorxor  44267  axc5c4c711  44363  pm2.43cbi  44481  euoreqb  47083  oppcendc  48980