Theorem dedth2h 4542

Description: Weak deduction theorem eliminating two hypotheses. This theorem is simpler to use than dedth2v 4545 but requires that each hypothesis have exactly one class variable. See also comments in dedth 4541. (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 4541	. . 3 ⊢ (𝜓 → 𝜃)
6	2, 5	dedth 4541	. 2 ⊢ (𝜑 → (𝜓 → 𝜒))
7	6	imp 412	1 ⊢ ((𝜑 ∧ 𝜓) → 𝜒)

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

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 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-if 4483

This theorem is used by:  dedth3h  4543  dedth4h  4544  dedth2v  4545  oawordeu  8547  oeoa  8590  unfilem3  9283  sqeqor  14340  binom2  14341  divalglem7  16549  divalg  16553  nmlno0  31379  ipassi  31425  sii  31438  ajfun  31444  ubth  31457  hvnegdi  31651  hvsubeq0  31652  normlem9at  31705  normsub0  31720  norm-ii  31722  norm-iii  31724  normsub  31727  normpyth  31729  norm3adifi  31737  normpar  31739  polid  31743  bcs  31765  shscl  31902  shslej  31964  shincl  31965  pjoc1  32018  pjoml  32020  pjoc2  32023  chincl  32083  chsscon3  32084  chlejb1  32096  chnle  32098  chdmm1  32109  spanun  32129  elspansn2  32151  h1datom  32166  cmbr3  32192  pjoml2  32195  pjoml3  32196  cmcm  32198  cmcm3  32199  lecm  32201  osum  32229  spansnj  32231  pjadji  32269  pjaddi  32270  pjsubi  32272  pjmuli  32273  pjch  32278  pj11  32298  pjnorm  32308  pjpyth  32309  pjnel  32310  hosubcl  32357  hoaddcom  32358  ho0sub  32381  honegsub  32383  eigre  32419  lnopeq0lem2  32590  lnopeq  32593  lnopunii  32596  lnophmi  32602  cvmd  32920  chrelat2  32954  cvexch  32958  mdsym  32996  kur14  35950  abs2sqle  36414  abs2sqlt  36415