Theorem dedth2h 4523

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

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 395   = wceq 1541  ifcif 4464

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1801  ax-4 1815  ax-5 1916  ax-6 1974  ax-7 2014  ax-8 2111  ax-9 2119  ax-ext 2710

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-ex 1786  df-sb 2071  df-clab 2717  df-cleq 2731  df-clel 2817  df-if 4465

This theorem is referenced by:  dedth3h  4524  dedth4h  4525  dedth2v  4526  oawordeu  8362  oeoa  8404  unfilem3  9041  eluzadd  12595  eluzsub  12596  sqeqor  13913  binom2  13914  divalglem7  16089  divalg  16093  nmlno0  29136  ipassi  29182  sii  29195  ajfun  29201  ubth  29214  hvnegdi  29408  hvsubeq0  29409  normlem9at  29462  normsub0  29477  norm-ii  29479  norm-iii  29481  normsub  29484  normpyth  29486  norm3adifi  29494  normpar  29496  polid  29500  bcs  29522  shscl  29659  shslej  29721  shincl  29722  pjoc1  29775  pjoml  29777  pjoc2  29780  chincl  29840  chsscon3  29841  chlejb1  29853  chnle  29855  chdmm1  29866  spanun  29886  elspansn2  29908  h1datom  29923  cmbr3  29949  pjoml2  29952  pjoml3  29953  cmcm  29955  cmcm3  29956  lecm  29958  osum  29986  spansnj  29988  pjadji  30026  pjaddi  30027  pjsubi  30029  pjmuli  30030  pjch  30035  pj11  30055  pjnorm  30065  pjpyth  30066  pjnel  30067  hosubcl  30114  hoaddcom  30115  ho0sub  30138  honegsub  30140  eigre  30176  lnopeq0lem2  30347  lnopeq  30350  lnopunii  30353  lnophmi  30359  cvmd  30677  chrelat2  30711  cvexch  30715  mdsym  30753  kur14  33157  abs2sqle  33617  abs2sqlt  33618