Theorem dedth2h 4484

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

Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 399   = wceq 1543  ifcif 4425

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2018  ax-8 2114  ax-9 2122  ax-ext 2708

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 848  df-ex 1788  df-sb 2073  df-clab 2715  df-cleq 2728  df-clel 2809  df-if 4426

This theorem is referenced by:  dedth3h  4485  dedth4h  4486  dedth2v  4487  oawordeu  8261  oeoa  8303  unfilem3  8915  eluzadd  12434  eluzsub  12435  sqeqor  13749  binom2  13750  divalglem7  15923  divalg  15927  nmlno0  28830  ipassi  28876  sii  28889  ajfun  28895  ubth  28908  hvnegdi  29102  hvsubeq0  29103  normlem9at  29156  normsub0  29171  norm-ii  29173  norm-iii  29175  normsub  29178  normpyth  29180  norm3adifi  29188  normpar  29190  polid  29194  bcs  29216  shscl  29353  shslej  29415  shincl  29416  pjoc1  29469  pjoml  29471  pjoc2  29474  chincl  29534  chsscon3  29535  chlejb1  29547  chnle  29549  chdmm1  29560  spanun  29580  elspansn2  29602  h1datom  29617  cmbr3  29643  pjoml2  29646  pjoml3  29647  cmcm  29649  cmcm3  29650  lecm  29652  osum  29680  spansnj  29682  pjadji  29720  pjaddi  29721  pjsubi  29723  pjmuli  29724  pjch  29729  pj11  29749  pjnorm  29759  pjpyth  29760  pjnel  29761  hosubcl  29808  hoaddcom  29809  ho0sub  29832  honegsub  29834  eigre  29870  lnopeq0lem2  30041  lnopeq  30044  lnopunii  30047  lnophmi  30053  cvmd  30371  chrelat2  30405  cvexch  30409  mdsym  30447  kur14  32845  abs2sqle  33305  abs2sqlt  33306