Theorem dedth2h 4538

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

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

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 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-if 4479

This theorem is referenced by:  dedth3h  4539  dedth4h  4540  dedth2v  4541  oawordeu  8480  oeoa  8522  unfilem3  9214  eluzaddOLD  12788  eluzsubOLD  12789  sqeqor  14141  binom2  14142  divalglem7  16328  divalg  16332  nmlno0  30757  ipassi  30803  sii  30816  ajfun  30822  ubth  30835  hvnegdi  31029  hvsubeq0  31030  normlem9at  31083  normsub0  31098  norm-ii  31100  norm-iii  31102  normsub  31105  normpyth  31107  norm3adifi  31115  normpar  31117  polid  31121  bcs  31143  shscl  31280  shslej  31342  shincl  31343  pjoc1  31396  pjoml  31398  pjoc2  31401  chincl  31461  chsscon3  31462  chlejb1  31474  chnle  31476  chdmm1  31487  spanun  31507  elspansn2  31529  h1datom  31544  cmbr3  31570  pjoml2  31573  pjoml3  31574  cmcm  31576  cmcm3  31577  lecm  31579  osum  31607  spansnj  31609  pjadji  31647  pjaddi  31648  pjsubi  31650  pjmuli  31651  pjch  31656  pj11  31676  pjnorm  31686  pjpyth  31687  pjnel  31688  hosubcl  31735  hoaddcom  31736  ho0sub  31759  honegsub  31761  eigre  31797  lnopeq0lem2  31968  lnopeq  31971  lnopunii  31974  lnophmi  31980  cvmd  32298  chrelat2  32332  cvexch  32336  mdsym  32374  kur14  35191  abs2sqle  35655  abs2sqlt  35656