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

Theorem pm5.21nd 898
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 432 . 2  |-  ( ph  ->  ( ps  ->  th )
)
3 pm5.21nd.2 . . 3  |-  ( (
ph  /\  ch )  ->  th )
43ex 432 . 2  |-  ( ph  ->  ( ch  ->  th )
)
5 pm5.21nd.3 . . 3  |-  ( th 
->  ( ps  <->  ch )
)
65a1i 11 . 2  |-  ( ph  ->  ( th  ->  ( ps 
<->  ch ) ) )
72, 4, 6pm5.21ndd 352 1  |-  ( ph  ->  ( ps  <->  ch )
)
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184    /\ wa 367
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 369
This theorem is referenced by:  ideqg  5067  fvelimab  5830  brrpssg  6481  ordsucelsuc  6556  releldm2  6749  relbrtpos  6884  relelec  7270  elfiun  7805  fpwwe2lem2  8921  fpwwelem  8934  fzrev3  11667  elfzp12  11679  eqgval  16367  eltg  19543  eltg2  19544  cncnp2  19868  isref  20095  islocfin  20103  isdivrngo  25550  opeldifid  27589  isfne  30323  opelopab3  30373  islshpkrN  35258  dihatexv2  37479
  Copyright terms: Public domain W3C validator