Theorem dedth3h 1788

Description: Weak deduction theorem eliminating three hypotheses.

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	. . . . 5 |- (A = if(ph, A, D) -> (th <-> ta ))
2	1	imbi2d 464	. . . 4 |- (A = if(ph, A, D) -> (((ps /\ ch) -> th) <-> ((ps /\ ch) -> ta )))
3		dedth3h.2	. . . . 5 |- (B = if(ps, B, R) -> (ta <-> et))
4		dedth3h.3	. . . . 5 |- (C = if(ch, C, S) -> (et <-> ze))
5		dedth3h.4	. . . . 5 |- ze
6	3, 4, 5	dedth2h 1787	. . . 4 |- ((ps /\ ch) -> ta )
7	2, 6	dedth 1784	. . 3 |- (ph -> ((ps /\ ch) -> th))
8	7	exp3a 292	. 2 |- (ph -> (ps -> (ch -> th)))
9	8	3imp 608	1 |- ((ph /\ ps /\ ch) -> th)

Syntax hints:   -> wi 2   <-> wb 127   /\ wa 196   /\ w3a 581   = wceq 1091  ifcif 1776

This theorem is referenced by:  addcant 4122  subaddt 4145  subdit 4184  mulcant 4208  divmult 4220  divdistrt 4246  ltadd1t 4348  leadd1t 4350  ltsubaddt 4353  lesubaddt 4355  ltdivt 4404  ltmuldivt 4406  ltdiv23t 4419  hvsubaddt 5042  omlsi 5250  shlubt 5355  chjasst 5446  spansncvt 5543  pjcjt2 5580  pjopytht 5662

This theorem was proved from axioms:  ax-1 3  ax-2 4  ax-3 5  ax-mp 6  ax-4 673  ax-5 674  ax-6 675  ax-7 676  ax-gen 677  ax-8 798  ax-9 799  ax-10 800  ax-11 801  ax-12 802  ax-16 922  ax-17 925  ax-ext 1074

This theorem depends on definitions:  df-bi 128  df-or 197  df-an 198  df-3an 583  df-ex 679  df-sb 853  df-clab 1093  df-cleq 1097  df-clel 1099  df-if 1777

metamath.org