Theorem dedth2h 4548

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

Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 400   = wceq 1570  ifcif 4488

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-if 4489

This theorem is referenced by:  dedth3h  4549  dedth4h  4550  dedth2v  4551  oawordeu  8541  oeoa  8584  unfilem3  9268  sqeqor  14254  binom2  14255  divalglem7  16458  divalg  16462  nmlno0  31128  ipassi  31174  sii  31187  ajfun  31193  ubth  31206  hvnegdi  31400  hvsubeq0  31401  normlem9at  31454  normsub0  31469  norm-ii  31471  norm-iii  31473  normsub  31476  normpyth  31478  norm3adifi  31486  normpar  31488  polid  31492  bcs  31514  shscl  31651  shslej  31713  shincl  31714  pjoc1  31767  pjoml  31769  pjoc2  31772  chincl  31832  chsscon3  31833  chlejb1  31845  chnle  31847  chdmm1  31858  spanun  31878  elspansn2  31900  h1datom  31915  cmbr3  31941  pjoml2  31944  pjoml3  31945  cmcm  31947  cmcm3  31948  lecm  31950  osum  31978  spansnj  31980  pjadji  32018  pjaddi  32019  pjsubi  32021  pjmuli  32022  pjch  32027  pj11  32047  pjnorm  32057  pjpyth  32058  pjnel  32059  hosubcl  32106  hoaddcom  32107  ho0sub  32130  honegsub  32132  eigre  32168  lnopeq0lem2  32339  lnopeq  32342  lnopunii  32345  lnophmi  32351  cvmd  32669  chrelat2  32703  cvexch  32707  mdsym  32745  kur14  35689  abs2sqle  36153  abs2sqlt  36154