Theorem ja 188

Description: Inference joining the antecedents of two premises. For partial converses, see jarri 108 and jarli 127. (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 17	. 2 ⊢ ((𝜑 → 𝜓) → (𝜑 → 𝜒))
3		ja.1	. 2 ⊢ (¬ 𝜑 → 𝜒)
4	2, 3	pm2.61d1 182	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  189  pm2.01  190  peirce  205  oibabs  966  pm2.74  990  pm5.71  1043  meredith  1668  tbw-bijust  1725  tbw-negdf  1726  merco1  1740  19.38  1866  19.35  1904  sbrimvw  2131  sbi2  2343  dfmoeu  2569  moabs  2577  exmoeu  2615  moanimlem  2652  r19.35  3129  r19.21v  3196  elab3gf  3652  elab3g  3653  dfss2  3931  r19.2zb  4466  ralidmw  4482  ralidm  4483  iununi  5069  asymref2  6118  nelaneqOLDOLD  9565  fsuppmapnn0fiub0  14028  itgeq2  25905  frgrwopreglem4a  30601  meran1  36810  imsym1  36817  bj-cbvaw  37151  bj-cbveaw  37153  bj-ssbid2ALT  37173  wl-moteq  38056  axc5c7  39574  axc5c711  39581  eu6w  43299  rp-fakeimass  44129  nanorxor  44906  axc5c4c711  45002  pm2.43cbi  45118  euoreqb  47734  oppcendc  49680