Theorem dedth2h 4607

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

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   = wceq 1537  ifcif 4548

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-if 4549

This theorem is referenced by:  dedth3h  4608  dedth4h  4609  dedth2v  4610  oawordeu  8611  oeoa  8653  unfilem3  9373  eluzaddOLD  12938  eluzsubOLD  12939  sqeqor  14265  binom2  14266  divalglem7  16447  divalg  16451  nmlno0  30827  ipassi  30873  sii  30886  ajfun  30892  ubth  30905  hvnegdi  31099  hvsubeq0  31100  normlem9at  31153  normsub0  31168  norm-ii  31170  norm-iii  31172  normsub  31175  normpyth  31177  norm3adifi  31185  normpar  31187  polid  31191  bcs  31213  shscl  31350  shslej  31412  shincl  31413  pjoc1  31466  pjoml  31468  pjoc2  31471  chincl  31531  chsscon3  31532  chlejb1  31544  chnle  31546  chdmm1  31557  spanun  31577  elspansn2  31599  h1datom  31614  cmbr3  31640  pjoml2  31643  pjoml3  31644  cmcm  31646  cmcm3  31647  lecm  31649  osum  31677  spansnj  31679  pjadji  31717  pjaddi  31718  pjsubi  31720  pjmuli  31721  pjch  31726  pj11  31746  pjnorm  31756  pjpyth  31757  pjnel  31758  hosubcl  31805  hoaddcom  31806  ho0sub  31829  honegsub  31831  eigre  31867  lnopeq0lem2  32038  lnopeq  32041  lnopunii  32044  lnophmi  32050  cvmd  32368  chrelat2  32402  cvexch  32406  mdsym  32444  kur14  35184  abs2sqle  35648  abs2sqlt  35649