Theorem dedth2h 4543

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

Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 400   = wceq 1563  ifcif 4483

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-8 2147  ax-9 2155  ax-ext 2737

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-ex 1803  df-sb 2094  df-clab 2744  df-cleq 2757  df-clel 2840  df-if 4484

This theorem is referenced by:  dedth3h  4544  dedth4h  4545  dedth2v  4546  oawordeu  8528  oeoa  8571  unfilem3  9255  sqeqor  14240  binom2  14241  divalglem7  16445  divalg  16449  nmlno0  31052  ipassi  31098  sii  31111  ajfun  31117  ubth  31130  hvnegdi  31324  hvsubeq0  31325  normlem9at  31378  normsub0  31393  norm-ii  31395  norm-iii  31397  normsub  31400  normpyth  31402  norm3adifi  31410  normpar  31412  polid  31416  bcs  31438  shscl  31575  shslej  31637  shincl  31638  pjoc1  31691  pjoml  31693  pjoc2  31696  chincl  31756  chsscon3  31757  chlejb1  31769  chnle  31771  chdmm1  31782  spanun  31802  elspansn2  31824  h1datom  31839  cmbr3  31865  pjoml2  31868  pjoml3  31869  cmcm  31871  cmcm3  31872  lecm  31874  osum  31902  spansnj  31904  pjadji  31942  pjaddi  31943  pjsubi  31945  pjmuli  31946  pjch  31951  pj11  31971  pjnorm  31981  pjpyth  31982  pjnel  31983  hosubcl  32030  hoaddcom  32031  ho0sub  32054  honegsub  32056  eigre  32092  lnopeq0lem2  32263  lnopeq  32266  lnopunii  32269  lnophmi  32275  cvmd  32593  chrelat2  32627  cvexch  32631  mdsym  32669  kur14  35574  abs2sqle  36038  abs2sqlt  36039