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

Theorem dedth2h 4090
 Description: Weak deduction theorem eliminating two hypotheses. This theorem is simpler to use than dedth2v 4093 but requires that each hypothesis has exactly one class variable. See also comments in dedth 4089. (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 329 . . 3 (𝐴 = if(𝜑, 𝐴, 𝐶) → ((𝜓𝜒) ↔ (𝜓𝜃)))
3 dedth2h.2 . . . 4 (𝐵 = if(𝜓, 𝐵, 𝐷) → (𝜃𝜏))
4 dedth2h.3 . . . 4 𝜏
53, 4dedth 4089 . . 3 (𝜓𝜃)
62, 5dedth 4089 . 2 (𝜑 → (𝜓𝜒))
76imp 444 1 ((𝜑𝜓) → 𝜒)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 195   ∧ wa 383   = wceq 1475  ifcif 4036 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590 This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-if 4037 This theorem is referenced by:  dedth3h  4091  dedth4h  4092  dedth2v  4093  oawordeu  7522  oeoa  7564  unfilem3  8111  eluzadd  11592  eluzsub  11593  sqeqor  12840  binom2  12841  divalglem7  14960  divalg  14964  nmlno0  27034  ipassi  27080  sii  27093  ajfun  27100  ubth  27113  hvnegdi  27308  hvsubeq0  27309  normlem9at  27362  normsub0  27377  norm-ii  27379  norm-iii  27381  normsub  27384  normpyth  27386  norm3adifi  27394  normpar  27396  polid  27400  bcs  27422  shscl  27561  shslej  27623  shincl  27624  pjoc1  27677  pjoml  27679  pjoc2  27682  chincl  27742  chsscon3  27743  chlejb1  27755  chnle  27757  chdmm1  27768  spanun  27788  elspansn2  27810  h1datom  27825  cmbr3  27851  pjoml2  27854  pjoml3  27855  cmcm  27857  cmcm3  27858  lecm  27860  osum  27888  spansnj  27890  pjadji  27928  pjaddi  27929  pjsubi  27931  pjmuli  27932  pjch  27937  pj11  27957  pjnorm  27967  pjpyth  27968  pjnel  27969  hosubcl  28016  hoaddcom  28017  ho0sub  28040  honegsub  28042  eigre  28078  lnopeq0lem2  28249  lnopeq  28252  lnopunii  28255  lnophmi  28261  cvmd  28579  chrelat2  28613  cvexch  28617  mdsym  28655  kur14  30452  abs2sqle  30828  abs2sqlt  30829
 Copyright terms: Public domain W3C validator