Theorem dedth3h 3016

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

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 674	. . 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 3015	. . 3 |- ((ps /\ ch) -> ta)
7	2, 6	dedth 3011	. 2 |- (ph -> ((ps /\ ch) -> th))
8	7	3impib 1065	1 |- ((ph /\ ps /\ ch) -> th)

Syntax hints:   -> wi 3   <-> wb 163   /\ wa 240   /\ w3a 858   = wceq 1298  ifcif 2982

This theorem is referenced by:  dedth3v 3019  addcan 6507  subadd 6532  ltadd1 6806  leadd1 6808  ltsubadd 6810  lesubadd 6812  mulcant2i 6879  divmul 6896  divdir 6933  div11 6941  ltmul1 7008  ltdiv1 7031  ltdiv1OLD 7032  ltmuldiv 7045  ltmuldivOLD 7046  icoshftf1olem 7579  icoun 7582  faclbnd4lem2 8201  efcnlem4 8687  ipdiri 9830  efifolem3 10078  hvaddcan 10569  hvsubadd 10577  norm3dif 10650  omlsii 10878  shlub 10987  chjass 11089  ledi 11096  spansncv 11233  pjcjt2 11272  pjopyth 11300  hoaddass 11345  hocsubdir 11348  hoddi 11552  dvdsle 13693  gcdaddm 13735  mulgcdlem6 13761  isumshft2 15830

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 1304  ax-gen 1305  ax-8 1306  ax-10 1308  ax-12 1310  ax-17 1317  ax-4 1319  ax-5o 1321  ax-6o 1324  ax-9o 1481  ax-10o 1500  ax-16 1580  ax-11o 1588  ax-ext 1865

This theorem depends on definitions:  df-bi 164  df-or 241  df-an 242  df-3an 860  df-ex 1327  df-sb 1536  df-clab 1872  df-cleq 1877  df-clel 1880  df-if 2983

Copyright terms: Public domain