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  1638  tbw-bijust  1695  tbw-negdf  1696  merco1  1710  19.38  1836  19.35  1875  sbi2  2301  dfmoeu  2534  moabs  2541  exmoeu  2579  moanimlem  2616  r19.35  3106  r19.35OLD  3107  r19.21v  3178  elab3gf  3687  elab3g  3688  dfss2  3981  r19.2zb  4502  ralidmw  4514  ralidm  4518  iununi  5104  asymref2  6140  nelaneq  9637  fsuppmapnn0fiub0  14031  itgeq2  25828  frgrwopreglem4a  30339  meran1  36394  imsym1  36401  bj-ssbid2ALT  36646  wl-moteq  37495  axc5c7  38893  axc5c711  38900  eu6w  42663  rp-fakeimass  43502  nanorxor  44301  axc5c4c711  44397  pm2.43cbi  44516  euoreqb  47059