Theorem dedth2h 4117

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

Syntax hints:   → wi 4   ↔ wb 196   ∧ wa 384   = wceq 1480  ifcif 4063

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1841  ax-6 1890  ax-7 1937  ax-9 2001  ax-10 2021  ax-11 2036  ax-12 2049  ax-13 2250  ax-ext 2606

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1883  df-clab 2613  df-cleq 2619  df-clel 2622  df-if 4064

This theorem is referenced by:  dedth3h  4118  dedth4h  4119  dedth2v  4120  oawordeu  7581  oeoa  7623  unfilem3  8171  eluzadd  11660  eluzsub  11661  sqeqor  12915  binom2  12916  divalglem7  15041  divalg  15045  nmlno0  27490  ipassi  27536  sii  27549  ajfun  27556  ubth  27569  hvnegdi  27764  hvsubeq0  27765  normlem9at  27818  normsub0  27833  norm-ii  27835  norm-iii  27837  normsub  27840  normpyth  27842  norm3adifi  27850  normpar  27852  polid  27856  bcs  27878  shscl  28017  shslej  28079  shincl  28080  pjoc1  28133  pjoml  28135  pjoc2  28138  chincl  28198  chsscon3  28199  chlejb1  28211  chnle  28213  chdmm1  28224  spanun  28244  elspansn2  28266  h1datom  28281  cmbr3  28307  pjoml2  28310  pjoml3  28311  cmcm  28313  cmcm3  28314  lecm  28316  osum  28344  spansnj  28346  pjadji  28384  pjaddi  28385  pjsubi  28387  pjmuli  28388  pjch  28393  pj11  28413  pjnorm  28423  pjpyth  28424  pjnel  28425  hosubcl  28472  hoaddcom  28473  ho0sub  28496  honegsub  28498  eigre  28534  lnopeq0lem2  28705  lnopeq  28708  lnopunii  28711  lnophmi  28717  cvmd  29035  chrelat2  29069  cvexch  29073  mdsym  29111  kur14  30898  abs2sqle  31274  abs2sqlt  31275