Theorem dedth2h 4527

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

Syntax hints:   → wi 4   ↔ wb 208   ∧ wa 398   = wceq 1536  ifcif 4470

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 1969  ax-7 2014  ax-8 2115  ax-9 2123  ax-ext 2796

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-ex 1780  df-sb 2069  df-clab 2803  df-cleq 2817  df-clel 2896  df-if 4471

This theorem is referenced by:  dedth3h  4528  dedth4h  4529  dedth2v  4530  oawordeu  8184  oeoa  8226  unfilem3  8787  eluzadd  12276  eluzsub  12277  sqeqor  13581  binom2  13582  divalglem7  15753  divalg  15757  nmlno0  28575  ipassi  28621  sii  28634  ajfun  28640  ubth  28653  hvnegdi  28847  hvsubeq0  28848  normlem9at  28901  normsub0  28916  norm-ii  28918  norm-iii  28920  normsub  28923  normpyth  28925  norm3adifi  28933  normpar  28935  polid  28939  bcs  28961  shscl  29098  shslej  29160  shincl  29161  pjoc1  29214  pjoml  29216  pjoc2  29219  chincl  29279  chsscon3  29280  chlejb1  29292  chnle  29294  chdmm1  29305  spanun  29325  elspansn2  29347  h1datom  29362  cmbr3  29388  pjoml2  29391  pjoml3  29392  cmcm  29394  cmcm3  29395  lecm  29397  osum  29425  spansnj  29427  pjadji  29465  pjaddi  29466  pjsubi  29468  pjmuli  29469  pjch  29474  pj11  29494  pjnorm  29504  pjpyth  29505  pjnel  29506  hosubcl  29553  hoaddcom  29554  ho0sub  29577  honegsub  29579  eigre  29615  lnopeq0lem2  29786  lnopeq  29789  lnopunii  29792  lnophmi  29798  cvmd  30116  chrelat2  30150  cvexch  30154  mdsym  30192  kur14  32467  abs2sqle  32927  abs2sqlt  32928