Theorem dedth2h 4173

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

Syntax hints:   → wi 4   ↔ wb 196   ∧ wa 383   = wceq 1523  ifcif 4119

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631

This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-clab 2638  df-cleq 2644  df-clel 2647  df-if 4120

This theorem is referenced by:  dedth3h  4174  dedth4h  4175  dedth2v  4176  oawordeu  7680  oeoa  7722  unfilem3  8267  eluzadd  11754  eluzsub  11755  sqeqor  13018  binom2  13019  divalglem7  15169  divalg  15173  nmlno0  27778  ipassi  27824  sii  27837  ajfun  27844  ubth  27857  hvnegdi  28052  hvsubeq0  28053  normlem9at  28106  normsub0  28121  norm-ii  28123  norm-iii  28125  normsub  28128  normpyth  28130  norm3adifi  28138  normpar  28140  polid  28144  bcs  28166  shscl  28305  shslej  28367  shincl  28368  pjoc1  28421  pjoml  28423  pjoc2  28426  chincl  28486  chsscon3  28487  chlejb1  28499  chnle  28501  chdmm1  28512  spanun  28532  elspansn2  28554  h1datom  28569  cmbr3  28595  pjoml2  28598  pjoml3  28599  cmcm  28601  cmcm3  28602  lecm  28604  osum  28632  spansnj  28634  pjadji  28672  pjaddi  28673  pjsubi  28675  pjmuli  28676  pjch  28681  pj11  28701  pjnorm  28711  pjpyth  28712  pjnel  28713  hosubcl  28760  hoaddcom  28761  ho0sub  28784  honegsub  28786  eigre  28822  lnopeq0lem2  28993  lnopeq  28996  lnopunii  28999  lnophmi  29005  cvmd  29323  chrelat2  29357  cvexch  29361  mdsym  29399  kur14  31324  abs2sqle  31700  abs2sqlt  31701