Theorem dedth2h 4090

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

Syntax hints:   → wi 4   ↔ wb 195   ∧ wa 383   = wceq 1475  ifcif 4036

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-if 4037

This theorem is referenced by:  dedth3h  4091  dedth4h  4092  dedth2v  4093  oawordeu  7522  oeoa  7564  unfilem3  8111  eluzadd  11592  eluzsub  11593  sqeqor  12840  binom2  12841  divalglem7  14960  divalg  14964  nmlno0  27034  ipassi  27080  sii  27093  ajfun  27100  ubth  27113  hvnegdi  27308  hvsubeq0  27309  normlem9at  27362  normsub0  27377  norm-ii  27379  norm-iii  27381  normsub  27384  normpyth  27386  norm3adifi  27394  normpar  27396  polid  27400  bcs  27422  shscl  27561  shslej  27623  shincl  27624  pjoc1  27677  pjoml  27679  pjoc2  27682  chincl  27742  chsscon3  27743  chlejb1  27755  chnle  27757  chdmm1  27768  spanun  27788  elspansn2  27810  h1datom  27825  cmbr3  27851  pjoml2  27854  pjoml3  27855  cmcm  27857  cmcm3  27858  lecm  27860  osum  27888  spansnj  27890  pjadji  27928  pjaddi  27929  pjsubi  27931  pjmuli  27932  pjch  27937  pj11  27957  pjnorm  27967  pjpyth  27968  pjnel  27969  hosubcl  28016  hoaddcom  28017  ho0sub  28040  honegsub  28042  eigre  28078  lnopeq0lem2  28249  lnopeq  28252  lnopunii  28255  lnophmi  28261  cvmd  28579  chrelat2  28613  cvexch  28617  mdsym  28655  kur14  30452  abs2sqle  30828  abs2sqlt  30829