Theorem dedth2h 4524

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

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 396   = wceq 1542  ifcif 4465

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1975  ax-7 2015  ax-8 2112  ax-9 2120  ax-ext 2711

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-ex 1787  df-sb 2072  df-clab 2718  df-cleq 2732  df-clel 2818  df-if 4466

This theorem is referenced by:  dedth3h  4525  dedth4h  4526  dedth2v  4527  oawordeu  8363  oeoa  8405  unfilem3  9050  eluzadd  12604  eluzsub  12605  sqeqor  13922  binom2  13923  divalglem7  16098  divalg  16102  nmlno0  29145  ipassi  29191  sii  29204  ajfun  29210  ubth  29223  hvnegdi  29417  hvsubeq0  29418  normlem9at  29471  normsub0  29486  norm-ii  29488  norm-iii  29490  normsub  29493  normpyth  29495  norm3adifi  29503  normpar  29505  polid  29509  bcs  29531  shscl  29668  shslej  29730  shincl  29731  pjoc1  29784  pjoml  29786  pjoc2  29789  chincl  29849  chsscon3  29850  chlejb1  29862  chnle  29864  chdmm1  29875  spanun  29895  elspansn2  29917  h1datom  29932  cmbr3  29958  pjoml2  29961  pjoml3  29962  cmcm  29964  cmcm3  29965  lecm  29967  osum  29995  spansnj  29997  pjadji  30035  pjaddi  30036  pjsubi  30038  pjmuli  30039  pjch  30044  pj11  30064  pjnorm  30074  pjpyth  30075  pjnel  30076  hosubcl  30123  hoaddcom  30124  ho0sub  30147  honegsub  30149  eigre  30185  lnopeq0lem2  30356  lnopeq  30359  lnopunii  30362  lnophmi  30368  cvmd  30686  chrelat2  30720  cvexch  30724  mdsym  30762  kur14  33166  abs2sqle  33626  abs2sqlt  33627