Theorem dedth2h 4588

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

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 397   = wceq 1542  ifcif 4529

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-if 4530

This theorem is referenced by:  dedth3h  4589  dedth4h  4590  dedth2v  4591  oawordeu  8555  oeoa  8597  unfilem3  9312  eluzaddOLD  12857  eluzsubOLD  12858  sqeqor  14180  binom2  14181  divalglem7  16342  divalg  16346  nmlno0  30079  ipassi  30125  sii  30138  ajfun  30144  ubth  30157  hvnegdi  30351  hvsubeq0  30352  normlem9at  30405  normsub0  30420  norm-ii  30422  norm-iii  30424  normsub  30427  normpyth  30429  norm3adifi  30437  normpar  30439  polid  30443  bcs  30465  shscl  30602  shslej  30664  shincl  30665  pjoc1  30718  pjoml  30720  pjoc2  30723  chincl  30783  chsscon3  30784  chlejb1  30796  chnle  30798  chdmm1  30809  spanun  30829  elspansn2  30851  h1datom  30866  cmbr3  30892  pjoml2  30895  pjoml3  30896  cmcm  30898  cmcm3  30899  lecm  30901  osum  30929  spansnj  30931  pjadji  30969  pjaddi  30970  pjsubi  30972  pjmuli  30973  pjch  30978  pj11  30998  pjnorm  31008  pjpyth  31009  pjnel  31010  hosubcl  31057  hoaddcom  31058  ho0sub  31081  honegsub  31083  eigre  31119  lnopeq0lem2  31290  lnopeq  31293  lnopunii  31296  lnophmi  31302  cvmd  31620  chrelat2  31654  cvexch  31658  mdsym  31696  kur14  34238  abs2sqle  34696  abs2sqlt  34697