Theorem dedth2h 4526

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

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   = wceq 1542  ifcif 4466

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-if 4467

This theorem is referenced by:  dedth3h  4527  dedth4h  4528  dedth2v  4529  oawordeu  8490  oeoa  8533  unfilem3  9217  sqeqor  14178  binom2  14179  divalglem7  16368  divalg  16372  nmlno0  30866  ipassi  30912  sii  30925  ajfun  30931  ubth  30944  hvnegdi  31138  hvsubeq0  31139  normlem9at  31192  normsub0  31207  norm-ii  31209  norm-iii  31211  normsub  31214  normpyth  31216  norm3adifi  31224  normpar  31226  polid  31230  bcs  31252  shscl  31389  shslej  31451  shincl  31452  pjoc1  31505  pjoml  31507  pjoc2  31510  chincl  31570  chsscon3  31571  chlejb1  31583  chnle  31585  chdmm1  31596  spanun  31616  elspansn2  31638  h1datom  31653  cmbr3  31679  pjoml2  31682  pjoml3  31683  cmcm  31685  cmcm3  31686  lecm  31688  osum  31716  spansnj  31718  pjadji  31756  pjaddi  31757  pjsubi  31759  pjmuli  31760  pjch  31765  pj11  31785  pjnorm  31795  pjpyth  31796  pjnel  31797  hosubcl  31844  hoaddcom  31845  ho0sub  31868  honegsub  31870  eigre  31906  lnopeq0lem2  32077  lnopeq  32080  lnopunii  32083  lnophmi  32089  cvmd  32407  chrelat2  32441  cvexch  32445  mdsym  32483  kur14  35398  abs2sqle  35862  abs2sqlt  35863