Theorem dedth2h 4527

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

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

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 4468

This theorem is referenced by:  dedth3h  4528  dedth4h  4529  dedth2v  4530  oawordeu  8483  oeoa  8526  unfilem3  9210  sqeqor  14169  binom2  14170  divalglem7  16359  divalg  16363  nmlno0  30881  ipassi  30927  sii  30940  ajfun  30946  ubth  30959  hvnegdi  31153  hvsubeq0  31154  normlem9at  31207  normsub0  31222  norm-ii  31224  norm-iii  31226  normsub  31229  normpyth  31231  norm3adifi  31239  normpar  31241  polid  31245  bcs  31267  shscl  31404  shslej  31466  shincl  31467  pjoc1  31520  pjoml  31522  pjoc2  31525  chincl  31585  chsscon3  31586  chlejb1  31598  chnle  31600  chdmm1  31611  spanun  31631  elspansn2  31653  h1datom  31668  cmbr3  31694  pjoml2  31697  pjoml3  31698  cmcm  31700  cmcm3  31701  lecm  31703  osum  31731  spansnj  31733  pjadji  31771  pjaddi  31772  pjsubi  31774  pjmuli  31775  pjch  31780  pj11  31800  pjnorm  31810  pjpyth  31811  pjnel  31812  hosubcl  31859  hoaddcom  31860  ho0sub  31883  honegsub  31885  eigre  31921  lnopeq0lem2  32092  lnopeq  32095  lnopunii  32098  lnophmi  32104  cvmd  32422  chrelat2  32456  cvexch  32460  mdsym  32498  kur14  35414  abs2sqle  35878  abs2sqlt  35879