Theorem dedth2h 4535

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

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   = wceq 1541  ifcif 4475

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-if 4476

This theorem is referenced by:  dedth3h  4536  dedth4h  4537  dedth2v  4538  oawordeu  8470  oeoa  8512  unfilem3  9191  eluzaddOLD  12767  eluzsubOLD  12768  sqeqor  14123  binom2  14124  divalglem7  16310  divalg  16314  nmlno0  30773  ipassi  30819  sii  30832  ajfun  30838  ubth  30851  hvnegdi  31045  hvsubeq0  31046  normlem9at  31099  normsub0  31114  norm-ii  31116  norm-iii  31118  normsub  31121  normpyth  31123  norm3adifi  31131  normpar  31133  polid  31137  bcs  31159  shscl  31296  shslej  31358  shincl  31359  pjoc1  31412  pjoml  31414  pjoc2  31417  chincl  31477  chsscon3  31478  chlejb1  31490  chnle  31492  chdmm1  31503  spanun  31523  elspansn2  31545  h1datom  31560  cmbr3  31586  pjoml2  31589  pjoml3  31590  cmcm  31592  cmcm3  31593  lecm  31595  osum  31623  spansnj  31625  pjadji  31663  pjaddi  31664  pjsubi  31666  pjmuli  31667  pjch  31672  pj11  31692  pjnorm  31702  pjpyth  31703  pjnel  31704  hosubcl  31751  hoaddcom  31752  ho0sub  31775  honegsub  31777  eigre  31813  lnopeq0lem2  31984  lnopeq  31987  lnopunii  31990  lnophmi  31996  cvmd  32314  chrelat2  32348  cvexch  32352  mdsym  32390  kur14  35258  abs2sqle  35722  abs2sqlt  35723