Theorem syl4 19

Description: Inference adding common consequents in an implication, thereby interchanging the original antecedent and consequent.

Hypothesis

Ref	Expression
syl4.1	|- (ph -> ps)

Assertion

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

Proof of Theorem syl4

Step	Hyp	Ref	Expression
1		syl4.1	. 2 |- (ph -> ps)
2		syl2 17	. 2 |- ((ph -> ps) -> ((ps -> ch) -> (ph -> ch)))
3	1, 2	ax-mp 6	1 |- ((ps -> ch) -> (ph -> ch))

Syntax hints:   -> wi 2

This theorem is referenced by:  syl34 20  syl5 22  syl7 24  pm2.86 63  loolin 66  loowoz 67  peirce 76  pm2.01 80  con2 82  imbi1i 161  dfor2 199  pm2.67 231  jaob 328  oibabs 493  dedlem0a 567  meredith 644  19.20 690  19.23 745  19.39 761  r19.37av 1300  axrep 1473  dmcosseq 2572  tz7.48lem 2993  kmlem1 3580  kmlem12 3591  axpowndlem2 3744  axacndlem4 3756  suppsr2 4017  suppsr3 4018  chcmh 5148  dmdbr 5731

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

metamath.org