Theorem dedth2h 4140

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

Hypotheses

Ref	Expression
dedth2h.1	|- ( A = if ( ph , A , C ) -> ( ch <-> th ) )
dedth2h.2	|- ( B = if ( ps , B , D ) -> ( th <-> ta ) )
dedth2h.3	|- ta

Assertion

Ref	Expression
dedth2h	|- ( ( ph /\ ps ) -> ch )

Proof of Theorem dedth2h

Step	Hyp	Ref	Expression
1		dedth2h.1	. . . 4 |- ( A = if ( ph , A , C ) -> ( ch <-> th ) )
2	1	imbi2d 330	. . 3 |- ( A = if ( ph , A , C ) -> ( ( ps -> ch ) <-> ( ps -> th ) ) )
3		dedth2h.2	. . . 4 |- ( B = if ( ps , B , D ) -> ( th <-> ta ) )
4		dedth2h.3	. . . 4 |- ta
5	3, 4	dedth 4139	. . 3 |- ( ps -> th )
6	2, 5	dedth 4139	. 2 |- ( ph -> ( ps -> ch ) )
7	6	imp 445	1 |- ( ( ph /\ ps ) -> ch )

Syntax hints:   -> wi 4   <-> wb 196   /\ wa 384   = wceq 1483   ifcif 4086

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-if 4087

This theorem is referenced by:  dedth3h  4141  dedth4h  4142  dedth2v  4143  oawordeu  7635  oeoa  7677  unfilem3  8226  eluzadd  11716  eluzsub  11717  sqeqor  12978  binom2  12979  divalglem7  15122  divalg  15126  nmlno0  27650  ipassi  27696  sii  27709  ajfun  27716  ubth  27729  hvnegdi  27924  hvsubeq0  27925  normlem9at  27978  normsub0  27993  norm-ii  27995  norm-iii  27997  normsub  28000  normpyth  28002  norm3adifi  28010  normpar  28012  polid  28016  bcs  28038  shscl  28177  shslej  28239  shincl  28240  pjoc1  28293  pjoml  28295  pjoc2  28298  chincl  28358  chsscon3  28359  chlejb1  28371  chnle  28373  chdmm1  28384  spanun  28404  elspansn2  28426  h1datom  28441  cmbr3  28467  pjoml2  28470  pjoml3  28471  cmcm  28473  cmcm3  28474  lecm  28476  osum  28504  spansnj  28506  pjadji  28544  pjaddi  28545  pjsubi  28547  pjmuli  28548  pjch  28553  pj11  28573  pjnorm  28583  pjpyth  28584  pjnel  28585  hosubcl  28632  hoaddcom  28633  ho0sub  28656  honegsub  28658  eigre  28694  lnopeq0lem2  28865  lnopeq  28868  lnopunii  28871  lnophmi  28877  cvmd  29195  chrelat2  29229  cvexch  29233  mdsym  29271  kur14  31198  abs2sqle  31574  abs2sqlt  31575