Theorem dedth2h 4585

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

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   = wceq 1540  ifcif 4525

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-if 4526

This theorem is referenced by:  dedth3h  4586  dedth4h  4587  dedth2v  4588  oawordeu  8593  oeoa  8635  unfilem3  9345  eluzaddOLD  12913  eluzsubOLD  12914  sqeqor  14255  binom2  14256  divalglem7  16436  divalg  16440  nmlno0  30814  ipassi  30860  sii  30873  ajfun  30879  ubth  30892  hvnegdi  31086  hvsubeq0  31087  normlem9at  31140  normsub0  31155  norm-ii  31157  norm-iii  31159  normsub  31162  normpyth  31164  norm3adifi  31172  normpar  31174  polid  31178  bcs  31200  shscl  31337  shslej  31399  shincl  31400  pjoc1  31453  pjoml  31455  pjoc2  31458  chincl  31518  chsscon3  31519  chlejb1  31531  chnle  31533  chdmm1  31544  spanun  31564  elspansn2  31586  h1datom  31601  cmbr3  31627  pjoml2  31630  pjoml3  31631  cmcm  31633  cmcm3  31634  lecm  31636  osum  31664  spansnj  31666  pjadji  31704  pjaddi  31705  pjsubi  31707  pjmuli  31708  pjch  31713  pj11  31733  pjnorm  31743  pjpyth  31744  pjnel  31745  hosubcl  31792  hoaddcom  31793  ho0sub  31816  honegsub  31818  eigre  31854  lnopeq0lem2  32025  lnopeq  32028  lnopunii  32031  lnophmi  32037  cvmd  32355  chrelat2  32389  cvexch  32393  mdsym  32431  kur14  35221  abs2sqle  35685  abs2sqlt  35686