Theorem pm5.21ndd 343

Description: Eliminate an antecedent implied by each side of a biconditional, deduction version. (Contributed by Paul Chapman, 21-Nov-2012.) (Proof shortened by Wolf Lammen, 6-Oct-2013.)

Hypotheses

Ref	Expression
pm5.21ndd.1	|- (ph -> (ch -> ps))
pm5.21ndd.2	|- (ph -> (th -> ps))
pm5.21ndd.3	|- (ph -> (ps -> (ch <-> th)))

Assertion

Ref	Expression
pm5.21ndd	|- (ph -> (ch <-> th))

Proof of Theorem pm5.21ndd

Step	Hyp	Ref	Expression
1		pm5.21ndd.3	. 2 |- (ph -> (ps -> (ch <-> th)))
2		pm5.21ndd.1	. . . 4 |- (ph -> (ch -> ps))
3	2	con3d 125	. . 3 |- (ph -> (-. ps -> -. ch))
4		pm5.21ndd.2	. . . 4 |- (ph -> (th -> ps))
5	4	con3d 125	. . 3 |- (ph -> (-. ps -> -. th))
6		pm5.21im 338	. . 3 |- (-. ch -> (-. th -> (ch <-> th)))
7	3, 5, 6	syl6c 60	. 2 |- (ph -> (-. ps -> (ch <-> th)))
8	1, 7	pm2.61d 150	1 |- (ph -> (ch <-> th))

Syntax hints:  -. wn 3   -> wi 4   <-> wb 176

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

This theorem depends on definitions:  df-bi 177

This theorem is referenced by:  pm5.21nd  868  rmob  3135  eqpw1uni  4331  fnasrn  5418  funiunfv  5468  eqncg  6127  eqtc  6162  elce  6176