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  2304  dfmoeu  2531  moabs  2538  exmoeu  2576  moanimlem  2613  r19.35  3090  r19.21v  3157  elab3gf  3635  elab3g  3636  dfss2  3915  r19.2zb  4443  ralidmw  4455  ralidm  4459  iununi  5045  asymref2  6063  nelaneqOLD  9488  fsuppmapnn0fiub0  13900  itgeq2  25706  frgrwopreglem4a  30290  meran1  36453  imsym1  36460  bj-ssbid2ALT  36705  wl-moteq  37556  axc5c7  38958  axc5c711  38965  eu6w  42717  rp-fakeimass  43553  nanorxor  44346  axc5c4c711  44442  pm2.43cbi  44559  euoreqb  47148  oppcendc  49058