Theorem dedth2h 4541

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

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

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-if 4482

This theorem is used by:  dedth3h  4542  dedth4h  4543  dedth2v  4544  oawordeu  8567  oeoa  8610  unfilem3  9303  sqeqor  14364  binom2  14365  divalglem7  16575  divalg  16579  nmlno0  31403  ipassi  31449  sii  31462  ajfun  31468  ubth  31481  hvnegdi  31675  hvsubeq0  31676  normlem9at  31729  normsub0  31744  norm-ii  31746  norm-iii  31748  normsub  31751  normpyth  31753  norm3adifi  31761  normpar  31763  polid  31767  bcs  31789  shscl  31926  shslej  31988  shincl  31989  pjoc1  32042  pjoml  32044  pjoc2  32047  chincl  32107  chsscon3  32108  chlejb1  32120  chnle  32122  chdmm1  32133  spanun  32153  elspansn2  32175  h1datom  32190  cmbr3  32216  pjoml2  32219  pjoml3  32220  cmcm  32222  cmcm3  32223  lecm  32225  osum  32253  spansnj  32255  pjadji  32293  pjaddi  32294  pjsubi  32296  pjmuli  32297  pjch  32302  pj11  32322  pjnorm  32332  pjpyth  32333  pjnel  32334  hosubcl  32381  hoaddcom  32382  ho0sub  32405  honegsub  32407  eigre  32443  lnopeq0lem2  32614  lnopeq  32617  lnopunii  32620  lnophmi  32626  cvmd  32944  chrelat2  32978  cvexch  32982  mdsym  33020  kur14  36068  abs2sqle  36532  abs2sqlt  36533