Theorem dedth2h 3994

Description: Weak deduction theorem eliminating two hypotheses. This theorem is simpler to use than dedth2v 3997 but requires that each hypothesis has exactly one class variable. See also comments in dedth 3993. (Contributed by NM, 15-May-1999.)

Hypotheses

Ref	Expression
dedth2h.1
dedth2h.2
dedth2h.3

Assertion

Ref	Expression
dedth2h

Proof of Theorem dedth2h

Step	Hyp	Ref	Expression
1		dedth2h.1	. . . 4
2	1	imbi2d 316	. . 3
3		dedth2h.2	. . . 4
4		dedth2h.3	. . . 4
5	3, 4	dedth 3993	. . 3
6	2, 5	dedth 3993	. 2
7	6	imp 429	1

Syntax hints:  ->wi 4  <->wb 184  /\wa 369  =wceq 1395  ifcif 3941

This theorem is referenced by:  dedth3h  3995  dedth4h  3996  dedth2v  3997  oawordeu  7223  oeoa  7265  unfilem3  7806  eluzadd  11138  eluzsub  11139  sqeqor  12282  binom2  12283  divalglem7  14057  divalg  14061  nmlno0  25710  ipassi  25756  sii  25769  ajfun  25776  ubth  25789  hvnegdi  25984  hvsubeq0  25985  normlem9at  26038  normsub0  26053  norm-ii  26055  norm-iii  26057  normsub  26060  normpyth  26062  norm3adifi  26070  normpar  26072  polid  26076  bcs  26098  shscl  26236  shslej  26298  shincl  26299  pjoc1  26352  pjoml  26354  pjoc2  26357  chincl  26417  chsscon3  26418  chlejb1  26430  chnle  26432  chdmm1  26443  spanun  26463  elspansn2  26485  h1datom  26500  cmbr3  26526  pjoml2  26529  pjoml3  26530  cmcm  26532  cmcm3  26533  lecm  26535  osum  26563  spansnj  26565  pjadji  26603  pjaddi  26604  pjsubi  26606  pjmuli  26607  pjch  26612  pj11  26632  pjnorm  26642  pjpyth  26643  pjnel  26644  hosubcl  26692  hoaddcom  26693  ho0sub  26716  honegsub  26718  eigre  26754  lnopeq0lem2  26925  lnopeq  26928  lnopunii  26931  lnophmi  26937  cvmd  27255  chrelat2  27289  cvexch  27293  mdsym  27331  kur14  28660  abs2sqle  29046  abs2sqlt  29047

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-clab 2443  df-cleq 2449  df-clel 2452  df-if 3942