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  952  pm2.74  975  pm5.71  1028  meredith  1639  tbw-bijust  1696  tbw-negdf  1697  merco1  1711  19.38  1837  19.35  1876  sbi2  2306  dfmoeu  2539  moabs  2546  exmoeu  2584  moanimlem  2621  r19.35  3114  r19.35OLD  3115  r19.21v  3186  elab3gf  3700  elab3g  3701  dfss2  3994  r19.2zb  4519  ralidmw  4531  ralidm  4535  iununi  5122  asymref2  6149  nelaneq  9668  fsuppmapnn0fiub0  14044  itgeq2  25833  frgrwopreglem4a  30342  meran1  36377  imsym1  36384  bj-ssbid2ALT  36629  wl-moteq  37468  axc5c7  38867  axc5c711  38874  eu6w  42631  rp-fakeimass  43474  nanorxor  44274  axc5c4c711  44370  pm2.43cbi  44489  euoreqb  47024