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

Theorem dedth3h 3980
Description: Weak deduction theorem eliminating three hypotheses. See comments in dedth2h 3979. (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 316 . . 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 3979 . . 3  |-  ( ( ps  /\  ch )  ->  ta )
72, 6dedth 3978 . 2  |-  ( ph  ->  ( ( ps  /\  ch )  ->  th )
)
873impib 1195 1  |-  ( (
ph  /\  ps  /\  ch )  ->  th )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184    /\ wa 369    /\ w3a 974    = wceq 1383   ifcif 3926
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1605  ax-4 1618  ax-5 1691  ax-6 1734  ax-7 1776  ax-10 1823  ax-11 1828  ax-12 1840  ax-13 1985  ax-ext 2421
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 976  df-tru 1386  df-ex 1600  df-nf 1604  df-sb 1727  df-clab 2429  df-cleq 2435  df-clel 2438  df-if 3927
This theorem is referenced by:  dedth3v  3983  faclbnd4lem2  12354  dvdsle  14013  gcdaddm  14149  ipdiri  25723  hvaddcan  25965  hvsubadd  25972  norm3dif  26045  omlsii  26299  chjass  26429  ledi  26436  spansncv  26549  pjcjt2  26588  pjopyth  26616  hoaddass  26679  hocsubdir  26682  hoddi  26887
  Copyright terms: Public domain W3C validator