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 340	. . 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 406	1 ⊢ ((𝜑 ∧ 𝜓) → 𝜒)

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   = wceq 1542  ifcif 4481

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-if 4482

This theorem is referenced by:  dedth3h  4542  dedth4h  4543  dedth2v  4544  oawordeu  8492  oeoa  8535  unfilem3  9219  sqeqor  14151  binom2  14152  divalglem7  16338  divalg  16342  nmlno0  30882  ipassi  30928  sii  30941  ajfun  30947  ubth  30960  hvnegdi  31154  hvsubeq0  31155  normlem9at  31208  normsub0  31223  norm-ii  31225  norm-iii  31227  normsub  31230  normpyth  31232  norm3adifi  31240  normpar  31242  polid  31246  bcs  31268  shscl  31405  shslej  31467  shincl  31468  pjoc1  31521  pjoml  31523  pjoc2  31526  chincl  31586  chsscon3  31587  chlejb1  31599  chnle  31601  chdmm1  31612  spanun  31632  elspansn2  31654  h1datom  31669  cmbr3  31695  pjoml2  31698  pjoml3  31699  cmcm  31701  cmcm3  31702  lecm  31704  osum  31732  spansnj  31734  pjadji  31772  pjaddi  31773  pjsubi  31775  pjmuli  31776  pjch  31781  pj11  31801  pjnorm  31811  pjpyth  31812  pjnel  31813  hosubcl  31860  hoaddcom  31861  ho0sub  31884  honegsub  31886  eigre  31922  lnopeq0lem2  32093  lnopeq  32096  lnopunii  32099  lnophmi  32105  cvmd  32423  chrelat2  32457  cvexch  32461  mdsym  32499  kur14  35429  abs2sqle  35893  abs2sqlt  35894