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

Theorem dedth3h 3697
Description: Weak deduction theorem eliminating three hypotheses. See comments in dedth2h 3696. (Contributed by NM, 15-May-1999.)
Hypotheses
Ref Expression
dedth3h.1  |-  ( A  =  if ( ph ,  A ,  D )  ->  ( th  <->  ta )
)
dedth3h.2  |-  ( B  =  if ( ps ,  B ,  R
)  ->  ( ta  <->  et ) )
dedth3h.3  |-  ( C  =  if ( ch ,  C ,  S
)  ->  ( et  <->  ze ) )
dedth3h.4  |-  ze
Assertion
Ref Expression
dedth3h  |-  ( (
ph  /\  ps  /\  ch )  ->  th )

Proof of Theorem dedth3h
StepHypRef Expression
1 dedth3h.1 . . . 4  |-  ( A  =  if ( ph ,  A ,  D )  ->  ( th  <->  ta )
)
21imbi2d 307 . . 3  |-  ( A  =  if ( ph ,  A ,  D )  ->  ( ( ( ps  /\  ch )  ->  th )  <->  ( ( ps  /\  ch )  ->  ta ) ) )
3 dedth3h.2 . . . 4  |-  ( B  =  if ( ps ,  B ,  R
)  ->  ( ta  <->  et ) )
4 dedth3h.3 . . . 4  |-  ( C  =  if ( ch ,  C ,  S
)  ->  ( et  <->  ze ) )
5 dedth3h.4 . . . 4  |-  ze
63, 4, 5dedth2h 3696 . . 3  |-  ( ( ps  /\  ch )  ->  ta )
72, 6dedth 3695 . 2  |-  ( ph  ->  ( ( ps  /\  ch )  ->  th )
)
873impib 1150 1  |-  ( (
ph  /\  ps  /\  ch )  ->  th )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176    /\ wa 358    /\ w3a 935    = wceq 1647   ifcif 3654
This theorem is referenced by:  dedth3v  3700  faclbnd4lem2  11472  dvdsle  12782  gcdaddm  12916  ipdiri  21721  hvaddcan  21962  hvsubadd  21969  norm3dif  22042  omlsii  22295  chjass  22425  ledi  22432  spansncv  22545  pjcjt2  22584  pjopyth  22612  hoaddass  22675  hocsubdir  22678  hoddi  22883
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1551  ax-5 1562  ax-17 1621  ax-9 1659  ax-8 1680  ax-6 1734  ax-7 1739  ax-11 1751  ax-12 1937  ax-ext 2347
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 937  df-tru 1324  df-ex 1547  df-nf 1550  df-sb 1654  df-clab 2353  df-cleq 2359  df-clel 2362  df-if 3655
  Copyright terms: Public domain W3C validator