Theorem pm5.21nd 679

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 599	. . 3 |- (ph -> (-. th -> (-. ps /\ -. ch)))
8		pm5.21 676	. . 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 3271  fvelimab 3756  fzrev3t 6454  climres 7050  climshft2 7051  iserzshft2 7052  iserzshft 7088  eltgt 7568  eltg2t 7569  iscld 7619  ismsg 7750  lmbr 7880  isring 8093

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