Theorem dedth2h 4524

Description: Weak deduction theorem eliminating two hypotheses. This theorem is simpler to use than dedth2v 4527 but requires that each hypothesis have exactly one class variable. See also comments in dedth 4523. (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 341	. . 3 ⊢ (𝐴 = if(𝜑, 𝐴, 𝐶) → ((𝜓 → 𝜒) ↔ (𝜓 → 𝜃)))
3		dedth2h.2	. . . 4 ⊢ (𝐵 = if(𝜓, 𝐵, 𝐷) → (𝜃 ↔ 𝜏))
4		dedth2h.3	. . . 4 ⊢ 𝜏
5	3, 4	dedth 4523	. . 3 ⊢ (𝜓 → 𝜃)
6	2, 5	dedth 4523	. 2 ⊢ (𝜑 → (𝜓 → 𝜒))
7	6	imp 408	1 ⊢ ((𝜑 ∧ 𝜓) → 𝜒)

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 397   = wceq 1539  ifcif 4465

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-ext 2707

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 846  df-ex 1780  df-sb 2066  df-clab 2714  df-cleq 2728  df-clel 2814  df-if 4466

This theorem is referenced by:  dedth3h  4525  dedth4h  4526  dedth2v  4527  oawordeu  8417  oeoa  8459  unfilem3  9124  eluzadd  12659  eluzsub  12660  sqeqor  13978  binom2  13979  divalglem7  16153  divalg  16157  nmlno0  29202  ipassi  29248  sii  29261  ajfun  29267  ubth  29280  hvnegdi  29474  hvsubeq0  29475  normlem9at  29528  normsub0  29543  norm-ii  29545  norm-iii  29547  normsub  29550  normpyth  29552  norm3adifi  29560  normpar  29562  polid  29566  bcs  29588  shscl  29725  shslej  29787  shincl  29788  pjoc1  29841  pjoml  29843  pjoc2  29846  chincl  29906  chsscon3  29907  chlejb1  29919  chnle  29921  chdmm1  29932  spanun  29952  elspansn2  29974  h1datom  29989  cmbr3  30015  pjoml2  30018  pjoml3  30019  cmcm  30021  cmcm3  30022  lecm  30024  osum  30052  spansnj  30054  pjadji  30092  pjaddi  30093  pjsubi  30095  pjmuli  30096  pjch  30101  pj11  30121  pjnorm  30131  pjpyth  30132  pjnel  30133  hosubcl  30180  hoaddcom  30181  ho0sub  30204  honegsub  30206  eigre  30242  lnopeq0lem2  30413  lnopeq  30416  lnopunii  30419  lnophmi  30425  cvmd  30743  chrelat2  30777  cvexch  30781  mdsym  30819  kur14  33223  abs2sqle  33683  abs2sqlt  33684