MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  pm5.21nd Unicode version

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
StepHypRef Expression
1 pm5.21nd.1 . . 3
21ex 434 . 2
3 pm5.21nd.2 . . 3
43ex 434 . 2
5 pm5.21nd.3 . . 3
65a1i 11 . 2
72, 4, 6pm5.21ndd 354 1
Colors of variables: wff setvar class
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
  Copyright terms: Public domain W3C validator