Theorem dedth2h 4539

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

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   = wceq 1541  ifcif 4479

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-if 4480

This theorem is referenced by:  dedth3h  4540  dedth4h  4541  dedth2v  4542  oawordeu  8482  oeoa  8525  unfilem3  9207  sqeqor  14139  binom2  14140  divalglem7  16326  divalg  16330  nmlno0  30870  ipassi  30916  sii  30929  ajfun  30935  ubth  30948  hvnegdi  31142  hvsubeq0  31143  normlem9at  31196  normsub0  31211  norm-ii  31213  norm-iii  31215  normsub  31218  normpyth  31220  norm3adifi  31228  normpar  31230  polid  31234  bcs  31256  shscl  31393  shslej  31455  shincl  31456  pjoc1  31509  pjoml  31511  pjoc2  31514  chincl  31574  chsscon3  31575  chlejb1  31587  chnle  31589  chdmm1  31600  spanun  31620  elspansn2  31642  h1datom  31657  cmbr3  31683  pjoml2  31686  pjoml3  31687  cmcm  31689  cmcm3  31690  lecm  31692  osum  31720  spansnj  31722  pjadji  31760  pjaddi  31761  pjsubi  31763  pjmuli  31764  pjch  31769  pj11  31789  pjnorm  31799  pjpyth  31800  pjnel  31801  hosubcl  31848  hoaddcom  31849  ho0sub  31872  honegsub  31874  eigre  31910  lnopeq0lem2  32081  lnopeq  32084  lnopunii  32087  lnophmi  32093  cvmd  32411  chrelat2  32445  cvexch  32449  mdsym  32487  kur14  35410  abs2sqle  35874  abs2sqlt  35875