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  948  pm2.74  971  pm5.71  1024  meredith  1645  tbw-bijust  1702  tbw-negdf  1703  merco1  1717  19.38  1842  19.35  1881  sbi2  2302  dfmoeu  2536  moabs  2543  exmoeu  2581  moanimlem  2620  r19.35  3268  elab3gf  3608  elab3g  3609  r19.2zb  4423  ralidmw  4435  ralidm  4439  iununi  5024  asymref2  6011  nelaneq  9288  fsuppmapnn0fiub0  13641  itgeq2  24847  frgrwopreglem4a  28575  meran1  34527  imsym1  34534  amosym1  34542  bj-ssbid2ALT  34771  wl-moteq  35600  axc5c7  36852  axc5c711  36859  rp-fakeimass  41017  nanorxor  41812  axc5c4c711  41908  pm2.43cbi  42027  euoreqb  44488