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  1642  tbw-bijust  1699  tbw-negdf  1700  merco1  1714  19.38  1840  19.35  1879  sbi2  2297  dfmoeu  2529  moabs  2536  exmoeu  2574  moanimlem  2613  r19.35  3107  r19.35OLD  3108  r19.21v  3178  elab3gf  3674  elab3g  3675  r19.2zb  4495  ralidmw  4507  ralidm  4511  iununi  5102  asymref2  6118  nelaneq  9600  fsuppmapnn0fiub0  13965  itgeq2  25627  frgrwopreglem4a  29996  meran1  35760  imsym1  35767  bj-ssbid2ALT  36004  wl-moteq  36847  axc5c7  38245  axc5c711  38252  rp-fakeimass  42726  nanorxor  43527  axc5c4c711  43623  pm2.43cbi  43742  euoreqb  46276