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  1642  tbw-bijust  1699  tbw-negdf  1700  merco1  1714  19.38  1840  19.35  1878  sbi2  2306  dfmoeu  2533  moabs  2541  exmoeu  2579  moanimlem  2616  r19.35  3092  r19.21v  3159  elab3gf  3637  elab3g  3638  dfss2  3917  r19.2zb  4451  ralidmw  4467  ralidm  4468  iununi  5052  asymref2  6072  nelaneqOLD  9505  fsuppmapnn0fiub0  13914  itgeq2  25733  frgrwopreglem4a  30334  meran1  36554  imsym1  36561  bj-ssbid2ALT  36807  wl-moteq  37658  axc5c7  39110  axc5c711  39117  eu6w  42861  rp-fakeimass  43695  nanorxor  44488  axc5c4c711  44584  pm2.43cbi  44701  euoreqb  47297  oppcendc  49205