Theorem dedth2h 4521

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

Syntax hints:   → wi 4   ↔ wb 207   ∧ wa 396   = wceq 1547  ifcif 4461

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2712

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-ex 1787  df-sb 2074  df-clab 2719  df-cleq 2732  df-clel 2815  df-if 4462

This theorem is referenced by:  dedth3h  4522  dedth4h  4523  dedth2v  4524  oawordeu  8487  oeoa  8530  unfilem3  9214  sqeqor  14176  binom2  14177  divalglem7  16366  divalg  16370  nmlno0  30891  ipassi  30937  sii  30950  ajfun  30956  ubth  30969  hvnegdi  31163  hvsubeq0  31164  normlem9at  31217  normsub0  31232  norm-ii  31234  norm-iii  31236  normsub  31239  normpyth  31241  norm3adifi  31249  normpar  31251  polid  31255  bcs  31277  shscl  31414  shslej  31476  shincl  31477  pjoc1  31530  pjoml  31532  pjoc2  31535  chincl  31595  chsscon3  31596  chlejb1  31608  chnle  31610  chdmm1  31621  spanun  31641  elspansn2  31663  h1datom  31678  cmbr3  31704  pjoml2  31707  pjoml3  31708  cmcm  31710  cmcm3  31711  lecm  31713  osum  31741  spansnj  31743  pjadji  31781  pjaddi  31782  pjsubi  31784  pjmuli  31785  pjch  31790  pj11  31810  pjnorm  31820  pjpyth  31821  pjnel  31822  hosubcl  31869  hoaddcom  31870  ho0sub  31893  honegsub  31895  eigre  31931  lnopeq0lem2  32102  lnopeq  32105  lnopunii  32108  lnophmi  32114  cvmd  32432  chrelat2  32466  cvexch  32470  mdsym  32508  kur14  35451  abs2sqle  35915  abs2sqlt  35916