Theorem dedth2h 4548

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

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   = wceq 1540  ifcif 4488

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 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-if 4489

This theorem is referenced by:  dedth3h  4549  dedth4h  4550  dedth2v  4551  oawordeu  8519  oeoa  8561  unfilem3  9256  eluzaddOLD  12828  eluzsubOLD  12829  sqeqor  14181  binom2  14182  divalglem7  16369  divalg  16373  nmlno0  30724  ipassi  30770  sii  30783  ajfun  30789  ubth  30802  hvnegdi  30996  hvsubeq0  30997  normlem9at  31050  normsub0  31065  norm-ii  31067  norm-iii  31069  normsub  31072  normpyth  31074  norm3adifi  31082  normpar  31084  polid  31088  bcs  31110  shscl  31247  shslej  31309  shincl  31310  pjoc1  31363  pjoml  31365  pjoc2  31368  chincl  31428  chsscon3  31429  chlejb1  31441  chnle  31443  chdmm1  31454  spanun  31474  elspansn2  31496  h1datom  31511  cmbr3  31537  pjoml2  31540  pjoml3  31541  cmcm  31543  cmcm3  31544  lecm  31546  osum  31574  spansnj  31576  pjadji  31614  pjaddi  31615  pjsubi  31617  pjmuli  31618  pjch  31623  pj11  31643  pjnorm  31653  pjpyth  31654  pjnel  31655  hosubcl  31702  hoaddcom  31703  ho0sub  31726  honegsub  31728  eigre  31764  lnopeq0lem2  31935  lnopeq  31938  lnopunii  31941  lnophmi  31947  cvmd  32265  chrelat2  32299  cvexch  32303  mdsym  32341  kur14  35203  abs2sqle  35667  abs2sqlt  35668