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  2308  dfmoeu  2535  moabs  2543  exmoeu  2581  moanimlem  2618  r19.35  3094  r19.21v  3161  elab3gf  3639  elab3g  3640  dfss2  3919  r19.2zb  4453  ralidmw  4469  ralidm  4470  iununi  5054  asymref2  6074  nelaneqOLD  9507  fsuppmapnn0fiub0  13916  itgeq2  25735  frgrwopreglem4a  30385  meran1  36605  imsym1  36612  bj-ssbid2ALT  36864  wl-moteq  37719  axc5c7  39171  axc5c711  39178  eu6w  42919  rp-fakeimass  43753  nanorxor  44546  axc5c4c711  44642  pm2.43cbi  44759  euoreqb  47355  oppcendc  49263