MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  dedth2h Structured version   Visualization version   GIF version

Theorem dedth2h 4482
Description: Weak deduction theorem eliminating two hypotheses. This theorem is simpler to use than dedth2v 4485 but requires that each hypothesis have exactly one class variable. See also comments in dedth 4481. (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
StepHypRef Expression
1 dedth2h.1 . . . 4 (𝐴 = if(𝜑, 𝐴, 𝐶) → (𝜒𝜃))
21imbi2d 344 . . 3 (𝐴 = if(𝜑, 𝐴, 𝐶) → ((𝜓𝜒) ↔ (𝜓𝜃)))
3 dedth2h.2 . . . 4 (𝐵 = if(𝜓, 𝐵, 𝐷) → (𝜃𝜏))
4 dedth2h.3 . . . 4 𝜏
53, 4dedth 4481 . . 3 (𝜓𝜃)
62, 5dedth 4481 . 2 (𝜑 → (𝜓𝜒))
76imp 410 1 ((𝜑𝜓) → 𝜒)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 209  wa 399   = wceq 1538  ifcif 4425
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2770
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-ex 1782  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-if 4426
This theorem is referenced by:  dedth3h  4483  dedth4h  4484  dedth2v  4485  oawordeu  8164  oeoa  8206  unfilem3  8768  eluzadd  12261  eluzsub  12262  sqeqor  13574  binom2  13575  divalglem7  15740  divalg  15744  nmlno0  28578  ipassi  28624  sii  28637  ajfun  28643  ubth  28656  hvnegdi  28850  hvsubeq0  28851  normlem9at  28904  normsub0  28919  norm-ii  28921  norm-iii  28923  normsub  28926  normpyth  28928  norm3adifi  28936  normpar  28938  polid  28942  bcs  28964  shscl  29101  shslej  29163  shincl  29164  pjoc1  29217  pjoml  29219  pjoc2  29222  chincl  29282  chsscon3  29283  chlejb1  29295  chnle  29297  chdmm1  29308  spanun  29328  elspansn2  29350  h1datom  29365  cmbr3  29391  pjoml2  29394  pjoml3  29395  cmcm  29397  cmcm3  29398  lecm  29400  osum  29428  spansnj  29430  pjadji  29468  pjaddi  29469  pjsubi  29471  pjmuli  29472  pjch  29477  pj11  29497  pjnorm  29507  pjpyth  29508  pjnel  29509  hosubcl  29556  hoaddcom  29557  ho0sub  29580  honegsub  29582  eigre  29618  lnopeq0lem2  29789  lnopeq  29792  lnopunii  29795  lnophmi  29801  cvmd  30119  chrelat2  30153  cvexch  30157  mdsym  30195  kur14  32573  abs2sqle  33033  abs2sqlt  33034
  Copyright terms: Public domain W3C validator