Theorem ja 152

Description: Inference joining the antecedents of two premises. (The proof was shortened by O'Cat, 19-Feb-2008.)

Hypotheses

Ref	Expression
ja.1	|- (-. ph -> ch)
ja.2	|- (ps -> ch)

Assertion

Ref	Expression
ja	|- ((ph -> ps) -> ch)

Proof of Theorem ja

Step	Hyp	Ref	Expression
1		ja.2	. . 3 |- (ps -> ch)
2	1	imim2i 11	. 2 |- ((ph -> ps) -> (ph -> ch))
3		ja.1	. 2 |- (-. ph -> ch)
4	2, 3	pm2.61d1 142	1 |- ((ph -> ps) -> ch)

Syntax hints:  -. wn 2   -> wi 3

This theorem is referenced by:  pm2.74 632  pm2.74OLD 633  pm5.18 722  pm5.71 820  meredith 1200  hbim 1354  ax46 1364  ax467 1370  hbimd 1468  sbi2 1603  mo2 1795  elab3gf 2408  elab3gOLD 2410  r19.2zb 2959  iununi 3331  tbw-bijust 14165  tbw-negdf 14166  merco1 14180  meran1 14235  imsym1 14242  amosym1 14250  ax4567 16359

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7

Copyright terms: Public domain