Theorem dedth2h 4530

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1805  ax-4 1819  ax-5 1920  ax-6 1977  ax-7 2018  ax-8 2134  ax-9 2142  ax-ext 2724

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 857  df-ex 1790  df-sb 2081  df-clab 2731  df-cleq 2744  df-clel 2827  df-if 4471

This theorem is referenced by:  dedth3h  4531  dedth4h  4532  dedth2v  4533  oawordeu  8508  oeoa  8551  unfilem3  9236  sqeqor  14215  binom2  14216  divalglem7  16405  divalg  16409  nmlno0  30933  ipassi  30979  sii  30992  ajfun  30998  ubth  31011  hvnegdi  31205  hvsubeq0  31206  normlem9at  31259  normsub0  31274  norm-ii  31276  norm-iii  31278  normsub  31281  normpyth  31283  norm3adifi  31291  normpar  31293  polid  31297  bcs  31319  shscl  31456  shslej  31518  shincl  31519  pjoc1  31572  pjoml  31574  pjoc2  31577  chincl  31637  chsscon3  31638  chlejb1  31650  chnle  31652  chdmm1  31663  spanun  31683  elspansn2  31705  h1datom  31720  cmbr3  31746  pjoml2  31749  pjoml3  31750  cmcm  31752  cmcm3  31753  lecm  31755  osum  31783  spansnj  31785  pjadji  31823  pjaddi  31824  pjsubi  31826  pjmuli  31827  pjch  31832  pj11  31852  pjnorm  31862  pjpyth  31863  pjnel  31864  hosubcl  31911  hoaddcom  31912  ho0sub  31935  honegsub  31937  eigre  31973  lnopeq0lem2  32144  lnopeq  32147  lnopunii  32150  lnophmi  32156  cvmd  32474  chrelat2  32508  cvexch  32512  mdsym  32550  kur14  35504  abs2sqle  35968  abs2sqlt  35969