Theorem dedth2h 4410

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

Syntax hints:   → wi 4   ↔ wb 198   ∧ wa 387   = wceq 1508  ifcif 4353

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1759  ax-4 1773  ax-5 1870  ax-6 1929  ax-7 1966  ax-8 2053  ax-9 2060  ax-ext 2752

This theorem depends on definitions:  df-bi 199  df-an 388  df-or 835  df-ex 1744  df-sb 2017  df-clab 2761  df-cleq 2773  df-clel 2848  df-if 4354

This theorem is referenced by:  dedth3h  4411  dedth4h  4412  dedth2v  4413  oawordeu  7988  oeoa  8030  unfilem3  8585  eluzadd  12093  eluzsub  12094  sqeqor  13399  binom2  13400  divalglem7  15616  divalg  15620  nmlno0  28364  ipassi  28410  sii  28423  ajfun  28430  ubth  28443  hvnegdi  28638  hvsubeq0  28639  normlem9at  28692  normsub0  28707  norm-ii  28709  norm-iii  28711  normsub  28714  normpyth  28716  norm3adifi  28724  normpar  28726  polid  28730  bcs  28752  shscl  28891  shslej  28953  shincl  28954  pjoc1  29007  pjoml  29009  pjoc2  29012  chincl  29072  chsscon3  29073  chlejb1  29085  chnle  29087  chdmm1  29098  spanun  29118  elspansn2  29140  h1datom  29155  cmbr3  29181  pjoml2  29184  pjoml3  29185  cmcm  29187  cmcm3  29188  lecm  29190  osum  29218  spansnj  29220  pjadji  29258  pjaddi  29259  pjsubi  29261  pjmuli  29262  pjch  29267  pj11  29287  pjnorm  29297  pjpyth  29298  pjnel  29299  hosubcl  29346  hoaddcom  29347  ho0sub  29370  honegsub  29372  eigre  29408  lnopeq0lem2  29579  lnopeq  29582  lnopunii  29585  lnophmi  29591  cvmd  29909  chrelat2  29943  cvexch  29947  mdsym  29985  kur14  32088  abs2sqle  32483  abs2sqlt  32484