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  4716  ideqg  4938  fvelimab  5685  releldm2  6297  relbrtpos  6387  brrpssg  6421  relelec  6842  elfiun  7330  fpwwe2lem2  8401  fpwwelem  8414  fzrev3  11002  elfzp12  11016  eqgval  14876  eltg  16912  eltg2  16913  cncnp2  17227  isdivrngo  21530  isfne  25860  isref  25871  islocfin  25888  opelopab3  25965  islshpkrN  29369  dihatexv2  31588
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