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

Theorem pm5.21nd 869
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 424 . 2  |-  ( ph  ->  ( ps  ->  th )
)
3 pm5.21nd.2 . . 3  |-  ( (
ph  /\  ch )  ->  th )
43ex 424 . 2  |-  ( ph  ->  ( ch  ->  th )
)
5 pm5.21nd.3 . . 3  |-  ( th 
->  ( ps  <->  ch )
)
65a1i 11 . 2  |-  ( ph  ->  ( th  ->  ( ps 
<->  ch ) ) )
72, 4, 6pm5.21ndd 344 1  |-  ( ph  ->  ( ps  <->  ch )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 177    /\ wa 359
This theorem is referenced by:  ordsucelsuc  4761  ideqg  4983  fvelimab  5741  releldm2  6356  relbrtpos  6449  brrpssg  6483  relelec  6904  elfiun  7393  fpwwe2lem2  8463  fpwwelem  8476  fzrev3  11067  elfzp12  11081  eqgval  14944  eltg  16977  eltg2  16978  cncnp2  17299  isdivrngo  21972  isfne  26238  isref  26249  islocfin  26266  opelopab3  26308  islshpkrN  29603  dihatexv2  31822
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 178  df-an 361
  Copyright terms: Public domain W3C validator