Theorem pm5.21nd 744

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 402	. . . . 5 |- (ph -> (ps -> th))
3	2	con3d 111	. . . 4 |- (ph -> (-. th -> -. ps))
4		pm5.21nd.2	. . . . . 6 |- ((ph /\ ch) -> th)
5	4	ex 402	. . . . 5 |- (ph -> (ch -> th))
6	5	con3d 111	. . . 4 |- (ph -> (-. th -> -. ch))
7	3, 6	jcad 661	. . 3 |- (ph -> (-. th -> (-. ps /\ -. ch)))
8		pm5.21 741	. . 3 |- ((-. ps /\ -. ch) -> (ps <-> ch))
9	7, 8	syl6 25	. 2 |- (ph -> (-. th -> (ps <-> ch)))
10		pm5.21nd.3	. 2 |- (th -> (ps <-> ch))
11	9, 10	pm2.61d2 143	1 |- (ph -> (ps <-> ch))

Syntax hints:  -. wn 2   -> wi 3   <-> wb 163   /\ wa 240

This theorem is referenced by:  ordsucelsuc 3902  ideqg 4114  ideqgOLD 4115  fvelimab 4725  fvelimabOLD 4726  fzrev3 7692  climresi 8365  climshft2i 8366  iserzshft2i 8367  iserzshfti 8404  eltg 8888  eltg2 8889  iscld 8945  ismsg 9077  lmbr 9206  isgalem 9449  isga2 9452  isring 9465  isflimf 10323  isdivrng 10417  ordsucuniel 13863  domrancur1b 14548  istopgrp 14971  elfiun 15369  isfne 15480  isref 15488  topfneec 15501  islocfin 15506  neibastop3 15524  limfilcf 15587  isfclus 15606  flimfcls 15613  opelopab3 15688  elfzp12 15795

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 164  df-an 242

Copyright terms: Public domain