Theorem dedth2h 4534

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

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   = wceq 1541  ifcif 4474

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-ex 1781  df-sb 2068  df-clab 2712  df-cleq 2725  df-clel 2808  df-if 4475

This theorem is referenced by:  dedth3h  4535  dedth4h  4536  dedth2v  4537  oawordeu  8476  oeoa  8518  unfilem3  9198  sqeqor  14125  binom2  14126  divalglem7  16312  divalg  16316  nmlno0  30777  ipassi  30823  sii  30836  ajfun  30842  ubth  30855  hvnegdi  31049  hvsubeq0  31050  normlem9at  31103  normsub0  31118  norm-ii  31120  norm-iii  31122  normsub  31125  normpyth  31127  norm3adifi  31135  normpar  31137  polid  31141  bcs  31163  shscl  31300  shslej  31362  shincl  31363  pjoc1  31416  pjoml  31418  pjoc2  31421  chincl  31481  chsscon3  31482  chlejb1  31494  chnle  31496  chdmm1  31507  spanun  31527  elspansn2  31549  h1datom  31564  cmbr3  31590  pjoml2  31593  pjoml3  31594  cmcm  31596  cmcm3  31597  lecm  31599  osum  31627  spansnj  31629  pjadji  31667  pjaddi  31668  pjsubi  31670  pjmuli  31671  pjch  31676  pj11  31696  pjnorm  31706  pjpyth  31707  pjnel  31708  hosubcl  31755  hoaddcom  31756  ho0sub  31779  honegsub  31781  eigre  31817  lnopeq0lem2  31988  lnopeq  31991  lnopunii  31994  lnophmi  32000  cvmd  32318  chrelat2  32352  cvexch  32356  mdsym  32394  kur14  35281  abs2sqle  35745  abs2sqlt  35746