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

Theorem dedth3h 3608
Description: Weak deduction theorem eliminating three hypotheses. See comments in dedth2h 3607. (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 3607 . . 3  |-  ( ( ps  /\  ch )  ->  ta )
72, 6dedth 3606 . 2  |-  ( ph  ->  ( ( ps  /\  ch )  ->  th )
)
873impib 1149 1  |-  ( (
ph  /\  ps  /\  ch )  ->  th )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176    /\ wa 358    /\ w3a 934    = wceq 1623   ifcif 3565
This theorem is referenced by:  dedth3v  3611  faclbnd4lem2  11307  dvdsle  12574  gcdaddm  12708  ipdiri  21408  hvaddcan  21649  hvsubadd  21656  norm3dif  21729  omlsii  21982  chjass  22112  ledi  22119  spansncv  22232  pjcjt2  22271  pjopyth  22299  hoaddass  22362  hocsubdir  22365  hoddi  22570
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-if 3566
  Copyright terms: Public domain W3C validator