Theorem dedth2h 4545

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401   = wceq 1570  ifcif 4485

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-if 4486

This theorem is used by:  dedth3h  4546  dedth4h  4547  dedth2v  4548  oawordeu  8594  oeoa  8637  unfilem3  9330  sqeqor  14390  binom2  14391  divalglem7  16601  divalg  16605  nmlno0  31430  ipassi  31476  sii  31489  ajfun  31495  ubth  31508  hvnegdi  31702  hvsubeq0  31703  normlem9at  31756  normsub0  31771  norm-ii  31773  norm-iii  31775  normsub  31778  normpyth  31780  norm3adifi  31788  normpar  31790  polid  31794  bcs  31816  shscl  31953  shslej  32015  shincl  32016  pjoc1  32069  pjoml  32071  pjoc2  32074  chincl  32134  chsscon3  32135  chlejb1  32147  chnle  32149  chdmm1  32160  spanun  32180  elspansn2  32202  h1datom  32217  cmbr3  32243  pjoml2  32246  pjoml3  32247  cmcm  32249  cmcm3  32250  lecm  32252  osum  32280  spansnj  32282  pjadji  32320  pjaddi  32321  pjsubi  32323  pjmuli  32324  pjch  32329  pj11  32349  pjnorm  32359  pjpyth  32360  pjnel  32361  hosubcl  32408  hoaddcom  32409  ho0sub  32432  honegsub  32434  eigre  32470  lnopeq0lem2  32641  lnopeq  32644  lnopunii  32647  lnophmi  32653  cvmd  32971  chrelat2  33005  cvexch  33009  mdsym  33047  kur14  36161  abs2sqle  36625  abs2sqlt  36626