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  4615  ideqg  4837  fvelimab  5580  releldm2  6172  relbrtpos  6247  brrpssg  6281  relelec  6702  elfiun  7185  fpwwe2lem2  8256  fpwwelem  8269  fzrev3  10851  elfzp12  10863  eqgval  14668  eltg  16697  eltg2  16698  cncnp2  17012  isdivrngo  21100  domrancur1b  25211  isfne  26279  isref  26290  islocfin  26307  opelopab3  26384  islshpkrN  29383  dihatexv2  31602
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