Theorem dedth2h 4592

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

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 394   = wceq 1534  ifcif 4533

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-ext 2697

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-ex 1775  df-sb 2061  df-clab 2704  df-cleq 2718  df-clel 2803  df-if 4534

This theorem is referenced by:  dedth3h  4593  dedth4h  4594  dedth2v  4595  oawordeu  8585  oeoa  8627  unfilem3  9346  eluzaddOLD  12909  eluzsubOLD  12910  sqeqor  14234  binom2  14235  divalglem7  16401  divalg  16405  nmlno0  30728  ipassi  30774  sii  30787  ajfun  30793  ubth  30806  hvnegdi  31000  hvsubeq0  31001  normlem9at  31054  normsub0  31069  norm-ii  31071  norm-iii  31073  normsub  31076  normpyth  31078  norm3adifi  31086  normpar  31088  polid  31092  bcs  31114  shscl  31251  shslej  31313  shincl  31314  pjoc1  31367  pjoml  31369  pjoc2  31372  chincl  31432  chsscon3  31433  chlejb1  31445  chnle  31447  chdmm1  31458  spanun  31478  elspansn2  31500  h1datom  31515  cmbr3  31541  pjoml2  31544  pjoml3  31545  cmcm  31547  cmcm3  31548  lecm  31550  osum  31578  spansnj  31580  pjadji  31618  pjaddi  31619  pjsubi  31621  pjmuli  31622  pjch  31627  pj11  31647  pjnorm  31657  pjpyth  31658  pjnel  31659  hosubcl  31706  hoaddcom  31707  ho0sub  31730  honegsub  31732  eigre  31768  lnopeq0lem2  31939  lnopeq  31942  lnopunii  31945  lnophmi  31951  cvmd  32269  chrelat2  32303  cvexch  32307  mdsym  32345  kur14  35044  abs2sqle  35508  abs2sqlt  35509