Theorem pm5.21nd 941

Description: Eliminate an antecedent implied by each side of a biconditional. (Contributed by NM, 20-Nov-2005.) (Proof shortened by Wolf Lammen, 4-Nov-2013.)

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	. . 3 |- ( ( ph /\ ps ) -> th )
2	1	ex 450	. 2 |- ( ph -> ( ps -> th ) )
3		pm5.21nd.2	. . 3 |- ( ( ph /\ ch ) -> th )
4	3	ex 450	. 2 |- ( ph -> ( ch -> th ) )
5		pm5.21nd.3	. . 3 |- ( th -> ( ps <-> ch ) )
6	5	a1i 11	. 2 |- ( ph -> ( th -> ( ps <-> ch ) ) )
7	2, 4, 6	pm5.21ndd 369	1 |- ( ph -> ( ps <-> ch ) )

Syntax hints:   -> wi 4   <-> wb 196   /\ wa 384

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 197  df-an 386

This theorem is referenced by:  ideqg  5273  fvelimab  6253  brrpssg  6939  ordsucelsuc  7022  releldm2  7218  relbrtpos  7363  relelec  7787  elfiun  8336  fpwwe2lem2  9454  fpwwelem  9467  fzrev3  12406  elfzp12  12419  eqgval  17643  eltg  20761  eltg2  20762  cncnp2  21085  isref  21312  islocfin  21320  opeldifid  29412  isfne  32334  opelopab3  33511  isdivrngo  33749  islshpkrN  34407  dihatexv2  36628