Theorem ja 153

Description: Inference joining the antecedents of two premises. (Contributed by NM, 5-Aug-1993.) (Proof shortened by 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 13	. 2 ⊢ ((φ → ψ) → (φ → χ))
3		ja.1	. 2 ⊢ (¬ φ → χ)
4	2, 3	pm2.61d1 151	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  154  pm2.61i  156  pm2.01  160  peirce  172  loolin  173  pm2.74  819  oibabs  851  pm5.71  902  dfnot  1332  meredith  1404  tbw-bijust  1463  tbw-negdf  1464  merco1  1478  19.38  1794  hbimOLD  1818  a16g  1945  sbi2  2064  ax46  2162  ax467  2169  mo2  2233  elab3gf  2991  r19.2zb  3641  iununi  4051