Theorem dedth2h 4537

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

Syntax hints:   → wi 4   ↔ wb 208   ∧ wa 399   = wceq 1559  ifcif 4477

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-ext 2733

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-ex 1799  df-sb 2090  df-clab 2740  df-cleq 2753  df-clel 2836  df-if 4478

This theorem is referenced by:  dedth3h  4538  dedth4h  4539  dedth2v  4540  oawordeu  8517  oeoa  8560  unfilem3  9244  sqeqor  14222  binom2  14223  divalglem7  16423  divalg  16427  nmlno0  30954  ipassi  31000  sii  31013  ajfun  31019  ubth  31032  hvnegdi  31226  hvsubeq0  31227  normlem9at  31280  normsub0  31295  norm-ii  31297  norm-iii  31299  normsub  31302  normpyth  31304  norm3adifi  31312  normpar  31314  polid  31318  bcs  31340  shscl  31477  shslej  31539  shincl  31540  pjoc1  31593  pjoml  31595  pjoc2  31598  chincl  31658  chsscon3  31659  chlejb1  31671  chnle  31673  chdmm1  31684  spanun  31704  elspansn2  31726  h1datom  31741  cmbr3  31767  pjoml2  31770  pjoml3  31771  cmcm  31773  cmcm3  31774  lecm  31776  osum  31804  spansnj  31806  pjadji  31844  pjaddi  31845  pjsubi  31847  pjmuli  31848  pjch  31853  pj11  31873  pjnorm  31883  pjpyth  31884  pjnel  31885  hosubcl  31932  hoaddcom  31933  ho0sub  31956  honegsub  31958  eigre  31994  lnopeq0lem2  32165  lnopeq  32168  lnopunii  32171  lnophmi  32177  cvmd  32495  chrelat2  32529  cvexch  32533  mdsym  32571  kur14  35526  abs2sqle  35990  abs2sqlt  35991