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  201  oibabs  951  pm2.74  974  pm5.71  1027  meredith  1644  tbw-bijust  1701  tbw-negdf  1702  merco1  1716  19.38  1842  19.35  1881  sbi2  2299  dfmoeu  2531  moabs  2538  exmoeu  2576  moanimlem  2615  r19.35  3109  r19.35OLD  3110  r19.21v  3180  elab3gf  3675  elab3g  3676  r19.2zb  4496  ralidmw  4508  ralidm  4512  iununi  5103  asymref2  6119  nelaneq  9594  fsuppmapnn0fiub0  13958  itgeq2  25295  frgrwopreglem4a  29563  meran1  35296  imsym1  35303  bj-ssbid2ALT  35540  wl-moteq  36383  axc5c7  37781  axc5c711  37788  rp-fakeimass  42263  nanorxor  43064  axc5c4c711  43160  pm2.43cbi  43279  euoreqb  45817