Theorem dedth3h 2392

Description: Weak deduction theorem eliminating three hypotheses. See comments in dedth2h 2391.

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

Step	Hyp	Ref	Expression
1		dedth3h.1	. . . 4 |- (A = if(ph, A, D) -> (th <-> ta))
2	1	imbi2d 614	. . 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
6	3, 4, 5	dedth2h 2391	. . 3 |- ((ps /\ ch) -> ta)
7	2, 6	dedth 2387	. 2 |- (ph -> ((ps /\ ch) -> th))
8	7	3impib 833	1 |- ((ph /\ ps /\ ch) -> th)

Syntax hints:   -> wi 3   <-> wb 146   /\ wa 223   /\ w3a 777   = wceq 958  ifcif 2365

This theorem is referenced by:  addcant 5364  subaddt 5387  ltadd1t 5635  leadd1t 5637  ltsubaddt 5639  lesubaddt 5641  mulcant2 5700  mulcant2OLD 5701  divmult 5719  divdirt 5757  divdirtOLD 5758  div11t 5766  ltmul1t 5832  ltdiv1t 5851  ltdiv1tOLD 5852  ltmuldivt 5865  ltmuldivtOLD 5866  icoshftf1olem 6411  icoun 6414  faclbnd4lem2 6949  efcnlem4 7422  ipdiri 8485  efifolem3 8719  hvaddcant 8932  hvsubaddt 8939  norm3dift 9012  omlsi 9240  shlubt 9349  chjasst 9451  ledit 9458  spansncvt 9593  pjcjt2 9632  pjopytht 9660  hoaddasst 9703  hocsubdirt 9706  hoddit 9910

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 964  ax-gen 965  ax-8 966  ax-10 968  ax-12 970  ax-17 973  ax-4 975  ax-5o 977  ax-6o 980  ax-9o 1125  ax-10o 1142  ax-16 1212  ax-11o 1220  ax-ext 1462

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-3an 779  df-ex 983  df-sb 1174  df-clab 1467  df-cleq 1472  df-clel 1475  df-if 2366

Copyright terms: Public domain