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  201  oibabs  949  pm2.74  972  pm5.71  1025  meredith  1644  tbw-bijust  1701  tbw-negdf  1702  merco1  1716  19.38  1841  19.35  1880  sbi2  2299  dfmoeu  2536  moabs  2543  exmoeu  2581  moanimlem  2620  r19.21v  3113  r19.35  3271  elab3gf  3615  elab3g  3616  r19.2zb  4426  ralidmw  4438  ralidm  4442  iununi  5028  asymref2  6022  nelaneq  9358  fsuppmapnn0fiub0  13713  itgeq2  24942  frgrwopreglem4a  28674  meran1  34600  imsym1  34607  amosym1  34615  bj-ssbid2ALT  34844  wl-moteq  35673  axc5c7  36925  axc5c711  36932  rp-fakeimass  41119  nanorxor  41923  axc5c4c711  42019  pm2.43cbi  42138  euoreqb  44601