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  203  oibabs  959  pm2.74  982  pm5.71  1035  meredith  1648  tbw-bijust  1705  tbw-negdf  1706  merco1  1720  19.38  1846  19.35  1884  sbi2  2313  dfmoeu  2539  moabs  2547  exmoeu  2585  moanimlem  2622  r19.35  3097  r19.21v  3164  elab3gf  3622  elab3g  3623  dfss2  3901  r19.2zb  4428  ralidmw  4444  ralidm  4445  iununi  5028  asymref2  6067  nelaneqOLDOLD  9509  fsuppmapnn0fiub0  13946  itgeq2  25763  frgrwopreglem4a  30398  meran1  36639  imsym1  36646  bj-cbvaw  36981  bj-cbveaw  36983  bj-ssbid2ALT  37003  wl-moteq  37885  axc5c7  39403  axc5c711  39410  eu6w  43126  rp-fakeimass  43956  nanorxor  44749  axc5c4c711  44845  pm2.43cbi  44962  euoreqb  47572  oppcendc  49508