Theorem dedth2h 4552

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401   = wceq 1570  ifcif 4492

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-ext 2738

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-ex 1813  df-sb 2100  df-clab 2745  df-cleq 2758  df-clel 2841  df-if 4493

This theorem is used by:  dedth3h  4553  dedth4h  4554  dedth2v  4555  oawordeu  8549  oeoa  8592  unfilem3  9277  sqeqor  14272  binom2  14273  divalglem7  16482  divalg  16486  nmlno0  31184  ipassi  31230  sii  31243  ajfun  31249  ubth  31262  hvnegdi  31456  hvsubeq0  31457  normlem9at  31510  normsub0  31525  norm-ii  31527  norm-iii  31529  normsub  31532  normpyth  31534  norm3adifi  31542  normpar  31544  polid  31548  bcs  31570  shscl  31707  shslej  31769  shincl  31770  pjoc1  31823  pjoml  31825  pjoc2  31828  chincl  31888  chsscon3  31889  chlejb1  31901  chnle  31903  chdmm1  31914  spanun  31934  elspansn2  31956  h1datom  31971  cmbr3  31997  pjoml2  32000  pjoml3  32001  cmcm  32003  cmcm3  32004  lecm  32006  osum  32034  spansnj  32036  pjadji  32074  pjaddi  32075  pjsubi  32077  pjmuli  32078  pjch  32083  pj11  32103  pjnorm  32113  pjpyth  32114  pjnel  32115  hosubcl  32162  hoaddcom  32163  ho0sub  32186  honegsub  32188  eigre  32224  lnopeq0lem2  32395  lnopeq  32398  lnopunii  32401  lnophmi  32407  cvmd  32725  chrelat2  32759  cvexch  32763  mdsym  32801  kur14  35729  abs2sqle  36193  abs2sqlt  36194