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  954  pm2.74  977  pm5.71  1030  meredith  1641  tbw-bijust  1698  tbw-negdf  1699  merco1  1713  19.38  1839  19.35  1877  sbi2  2302  dfmoeu  2536  moabs  2543  exmoeu  2581  moanimlem  2618  r19.35  3108  r19.35OLD  3109  r19.21v  3180  elab3gf  3684  elab3g  3685  dfss2  3969  r19.2zb  4496  ralidmw  4508  ralidm  4512  iununi  5099  asymref2  6137  nelaneq  9639  fsuppmapnn0fiub0  14034  itgeq2  25813  frgrwopreglem4a  30329  meran1  36412  imsym1  36419  bj-ssbid2ALT  36664  wl-moteq  37515  axc5c7  38912  axc5c711  38919  eu6w  42686  rp-fakeimass  43525  nanorxor  44324  axc5c4c711  44420  pm2.43cbi  44538  euoreqb  47121  oppcendc  48906