Theorem dedth2h 4545

Description: Weak deduction theorem eliminating two hypotheses. This theorem is simpler to use than dedth2v 4548 but requires that each hypothesis have exactly one class variable. See also comments in dedth 4544. (Contributed by NM, 15-May-1999.)

Hypotheses

Ref	Expression
dedth2h.1	⊢ (𝐴 = if(𝜑, 𝐴, 𝐶) → (𝜒 ↔ 𝜃))
dedth2h.2	⊢ (𝐵 = if(𝜓, 𝐵, 𝐷) → (𝜃 ↔ 𝜏))
dedth2h.3	⊢ 𝜏

Assertion

Ref	Expression
dedth2h	⊢ ((𝜑 ∧ 𝜓) → 𝜒)

Proof of Theorem dedth2h

Step	Hyp	Ref	Expression
1		dedth2h.1	. . . 4 ⊢ (𝐴 = if(𝜑, 𝐴, 𝐶) → (𝜒 ↔ 𝜃))
2	1	imbi2d 343	. . 3 ⊢ (𝐴 = if(𝜑, 𝐴, 𝐶) → ((𝜓 → 𝜒) ↔ (𝜓 → 𝜃)))
3		dedth2h.2	. . . 4 ⊢ (𝐵 = if(𝜓, 𝐵, 𝐷) → (𝜃 ↔ 𝜏))
4		dedth2h.3	. . . 4 ⊢ 𝜏
5	3, 4	dedth 4544	. . 3 ⊢ (𝜓 → 𝜃)
6	2, 5	dedth 4544	. 2 ⊢ (𝜑 → (𝜓 → 𝜒))
7	6	imp 412	1 ⊢ ((𝜑 ∧ 𝜓) → 𝜒)

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401   = wceq 1570  ifcif 4485

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2734

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-ex 1813  df-sb 2100  df-clab 2741  df-cleq 2754  df-clel 2837  df-if 4486

This theorem is used by:  dedth3h  4546  dedth4h  4547  dedth2v  4548  oawordeu  8546  oeoa  8589  unfilem3  9281  sqeqor  14284  binom2  14285  divalglem7  16495  divalg  16499  nmlno0  31284  ipassi  31330  sii  31343  ajfun  31349  ubth  31362  hvnegdi  31556  hvsubeq0  31557  normlem9at  31610  normsub0  31625  norm-ii  31627  norm-iii  31629  normsub  31632  normpyth  31634  norm3adifi  31642  normpar  31644  polid  31648  bcs  31670  shscl  31807  shslej  31869  shincl  31870  pjoc1  31923  pjoml  31925  pjoc2  31928  chincl  31988  chsscon3  31989  chlejb1  32001  chnle  32003  chdmm1  32014  spanun  32034  elspansn2  32056  h1datom  32071  cmbr3  32097  pjoml2  32100  pjoml3  32101  cmcm  32103  cmcm3  32104  lecm  32106  osum  32134  spansnj  32136  pjadji  32174  pjaddi  32175  pjsubi  32177  pjmuli  32178  pjch  32183  pj11  32203  pjnorm  32213  pjpyth  32214  pjnel  32215  hosubcl  32262  hoaddcom  32263  ho0sub  32286  honegsub  32288  eigre  32324  lnopeq0lem2  32495  lnopeq  32498  lnopunii  32501  lnophmi  32507  cvmd  32825  chrelat2  32859  cvexch  32863  mdsym  32901  kur14  35803  abs2sqle  36267  abs2sqlt  36268