Theorem pm5.21nd 900

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
pm5.21nd.2
pm5.21nd.3

Assertion

Ref	Expression
pm5.21nd

Proof of Theorem pm5.21nd

Step	Hyp	Ref	Expression
1		pm5.21nd.1	. . 3
2	1	ex 434	. 2
3		pm5.21nd.2	. . 3
4	3	ex 434	. 2
5		pm5.21nd.3	. . 3
6	5	a1i 11	. 2
7	2, 4, 6	pm5.21ndd 354	1

Syntax hints:  ->wi 4  <->wb 184  /\wa 369

This theorem is referenced by:  ideqg  5159  fvelimab  5929  brrpssg  6582  ordsucelsuc  6657  releldm2  6850  relbrtpos  6985  relelec  7371  elfiun  7910  fpwwe2lem2  9031  fpwwelem  9044  fzrev3  11774  elfzp12  11786  eqgval  16250  eltg  19458  eltg2  19459  cncnp2  19782  isref  20010  islocfin  20018  isdivrngo  25433  opeldifid  27456  isfne  30157  opelopab3  30207  islshpkrN  34845  dihatexv2  37066

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 185  df-an 371