Theorem ja 187

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 181	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  188  pm2.01  189  peirce  204  oibabs  964  pm2.74  988  pm5.71  1041  meredith  1661  tbw-bijust  1718  tbw-negdf  1719  merco1  1733  19.38  1859  19.35  1897  sbrimvw  2124  sbi2  2336  dfmoeu  2562  moabs  2570  exmoeu  2608  moanimlem  2645  r19.35  3120  r19.21v  3187  elab3gf  3643  elab3g  3644  dfss2  3922  r19.2zb  4454  ralidmw  4470  ralidm  4471  iununi  5056  asymref2  6104  nelaneqOLDOLD  9552  fsuppmapnn0fiub0  14006  itgeq2  25840  frgrwopreglem4a  30512  meran1  36771  imsym1  36778  bj-cbvaw  37113  bj-cbveaw  37115  bj-ssbid2ALT  37135  wl-moteq  38017  axc5c7  39535  axc5c711  39542  eu6w  43258  rp-fakeimass  44088  nanorxor  44881  axc5c4c711  44977  pm2.43cbi  45094  euoreqb  47703  oppcendc  49639