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

Theorem pm5.21nd 868
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
StepHypRef Expression
1 pm5.21nd.1 . . 3  |-  ( (
ph  /\  ps )  ->  th )
21ex 423 . 2  |-  ( ph  ->  ( ps  ->  th )
)
3 pm5.21nd.2 . . 3  |-  ( (
ph  /\  ch )  ->  th )
43ex 423 . 2  |-  ( ph  ->  ( ch  ->  th )
)
5 pm5.21nd.3 . . 3  |-  ( th 
->  ( ps  <->  ch )
)
65a1i 10 . 2  |-  ( ph  ->  ( th  ->  ( ps 
<->  ch ) ) )
72, 4, 6pm5.21ndd 343 1  |-  ( ph  ->  ( ps  <->  ch )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176    /\ wa 358
This theorem is referenced by:  ordsucelsuc  4613  ideqg  4835  fvelimab  5578  releldm2  6170  relbrtpos  6245  brrpssg  6279  relelec  6700  elfiun  7183  fpwwe2lem2  8254  fpwwelem  8267  fzrev3  10849  elfzp12  10861  eqgval  14666  eltg  16695  eltg2  16696  cncnp2  17010  isdivrngo  21098  domrancur1b  25200  isfne  26268  isref  26279  islocfin  26296  opelopab3  26373  islshpkrN  29310  dihatexv2  31529
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 177  df-an 360
  Copyright terms: Public domain W3C validator