Theorem dedth2h 4590

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

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   = wceq 1537  ifcif 4531

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-ex 1777  df-sb 2063  df-clab 2713  df-cleq 2727  df-clel 2814  df-if 4532

This theorem is referenced by:  dedth3h  4591  dedth4h  4592  dedth2v  4593  oawordeu  8592  oeoa  8634  unfilem3  9343  eluzaddOLD  12911  eluzsubOLD  12912  sqeqor  14252  binom2  14253  divalglem7  16433  divalg  16437  nmlno0  30824  ipassi  30870  sii  30883  ajfun  30889  ubth  30902  hvnegdi  31096  hvsubeq0  31097  normlem9at  31150  normsub0  31165  norm-ii  31167  norm-iii  31169  normsub  31172  normpyth  31174  norm3adifi  31182  normpar  31184  polid  31188  bcs  31210  shscl  31347  shslej  31409  shincl  31410  pjoc1  31463  pjoml  31465  pjoc2  31468  chincl  31528  chsscon3  31529  chlejb1  31541  chnle  31543  chdmm1  31554  spanun  31574  elspansn2  31596  h1datom  31611  cmbr3  31637  pjoml2  31640  pjoml3  31641  cmcm  31643  cmcm3  31644  lecm  31646  osum  31674  spansnj  31676  pjadji  31714  pjaddi  31715  pjsubi  31717  pjmuli  31718  pjch  31723  pj11  31743  pjnorm  31753  pjpyth  31754  pjnel  31755  hosubcl  31802  hoaddcom  31803  ho0sub  31826  honegsub  31828  eigre  31864  lnopeq0lem2  32035  lnopeq  32038  lnopunii  32041  lnophmi  32047  cvmd  32365  chrelat2  32399  cvexch  32403  mdsym  32441  kur14  35201  abs2sqle  35665  abs2sqlt  35666