Theorem dedth3h 2378

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

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 610	. . 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 2377	. . 3 |- ((ps /\ ch) -> ta)
7	2, 6	dedth 2373	. 2 |- (ph -> ((ps /\ ch) -> th))
8	7	3impib 829	1 |- ((ph /\ ps /\ ch) -> th)

Syntax hints:   -> wi 3   <-> wb 146   /\ wa 223   /\ w3a 773   = wceq 953  ifcif 2351

This theorem is referenced by:  addcant 5324  subaddt 5347  ltadd1t 5597  leadd1t 5599  ltsubaddt 5601  lesubaddt 5603  mulcant2 5660  divmult 5676  divdirt 5713  div11t 5721  ltmul1t 5786  ltdiv1t 5805  ltmuldivt 5817  icoshftf1olem 6343  icoun 6346  faclbnd4lem2 6886  efcnlem4 7362  ipdiri 8420  efifolem3 8639  hvaddcant 8858  hvsubaddt 8865  norm3dift 8938  omlsi 9160  shlubt 9269  chjasst 9371  ledit 9378  spansncvt 9515  pjcjt2 9554  pjopytht 9582  hoaddasst 9625  hocsubdirt 9628  hoddit 9830

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 959  ax-gen 960  ax-8 961  ax-10 963  ax-12 965  ax-17 968  ax-4 970  ax-5o 972  ax-6o 975  ax-9o 1119  ax-10o 1136  ax-16 1206  ax-11o 1213  ax-ext 1452

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-3an 775  df-ex 978  df-sb 1168  df-clab 1457  df-cleq 1462  df-clel 1465  df-if 2352

Copyright terms: Public domain