Theorem dedth2h 4565

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

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   = wceq 1540  ifcif 4505

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 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-ex 1780  df-sb 2066  df-clab 2715  df-cleq 2728  df-clel 2810  df-if 4506

This theorem is referenced by:  dedth3h  4566  dedth4h  4567  dedth2v  4568  oawordeu  8572  oeoa  8614  unfilem3  9322  eluzaddOLD  12892  eluzsubOLD  12893  sqeqor  14239  binom2  14240  divalglem7  16423  divalg  16427  nmlno0  30781  ipassi  30827  sii  30840  ajfun  30846  ubth  30859  hvnegdi  31053  hvsubeq0  31054  normlem9at  31107  normsub0  31122  norm-ii  31124  norm-iii  31126  normsub  31129  normpyth  31131  norm3adifi  31139  normpar  31141  polid  31145  bcs  31167  shscl  31304  shslej  31366  shincl  31367  pjoc1  31420  pjoml  31422  pjoc2  31425  chincl  31485  chsscon3  31486  chlejb1  31498  chnle  31500  chdmm1  31511  spanun  31531  elspansn2  31553  h1datom  31568  cmbr3  31594  pjoml2  31597  pjoml3  31598  cmcm  31600  cmcm3  31601  lecm  31603  osum  31631  spansnj  31633  pjadji  31671  pjaddi  31672  pjsubi  31674  pjmuli  31675  pjch  31680  pj11  31700  pjnorm  31710  pjpyth  31711  pjnel  31712  hosubcl  31759  hoaddcom  31760  ho0sub  31783  honegsub  31785  eigre  31821  lnopeq0lem2  31992  lnopeq  31995  lnopunii  31998  lnophmi  32004  cvmd  32322  chrelat2  32356  cvexch  32360  mdsym  32398  kur14  35243  abs2sqle  35707  abs2sqlt  35708