Theorem pm5.21nd 684

Description: Eliminate an antecedent implied by each side of a biconditional.

Hypotheses

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

Assertion

Ref	Expression
pm5.21nd	|- (ph -> (ps <-> ch))

Proof of Theorem pm5.21nd

Step	Hyp	Ref	Expression
1		pm5.21nd.1	. . . . . 6 |- ((ph /\ ps) -> th)
2	1	ex 373	. . . . 5 |- (ph -> (ps -> th))
3	2	con3d 95	. . . 4 |- (ph -> (-. th -> -. ps))
4		pm5.21nd.2	. . . . . 6 |- ((ph /\ ch) -> th)
5	4	ex 373	. . . . 5 |- (ph -> (ch -> th))
6	5	con3d 95	. . . 4 |- (ph -> (-. th -> -. ch))
7	3, 6	jcad 603	. . 3 |- (ph -> (-. th -> (-. ps /\ -. ch)))
8		pm5.21 681	. . 3 |- ((-. ps /\ -. ch) -> (ps <-> ch))
9	7, 8	syl6 22	. 2 |- (ph -> (-. th -> (ps <-> ch)))
10		pm5.21nd.3	. 2 |- (th -> (ps <-> ch))
11	9, 10	pm2.61d2 129	1 |- (ph -> (ps <-> ch))

Syntax hints:  -. wn 2   -> wi 3   <-> wb 146   /\ wa 223

This theorem is referenced by:  ideqg 3290  fvelimab 3779  fzrev3t 6464  climres 7119  climshft2 7120  iserzshft2 7121  iserzshft 7158  eltgt 7630  eltg2t 7631  iscld 7678  ismsg 7809  lmbr 7937  isring 8149

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

This theorem depends on definitions:  df-bi 147  df-an 225

Copyright terms: Public domain