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

Theorem dedth2h 4284
Description: Weak deduction theorem eliminating two hypotheses. This theorem is simpler to use than dedth2v 4287 but requires that each hypothesis has exactly one class variable. See also comments in dedth 4283. (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 4283 . . 3 (𝜓𝜃)
62, 5dedth 4283 . 2 (𝜑 → (𝜓𝜒))
76imp 444 1 ((𝜑𝜓) → 𝜒)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wa 383   = wceq 1632  ifcif 4230
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1988  ax-6 2054  ax-7 2090  ax-9 2148  ax-10 2168  ax-11 2183  ax-12 2196  ax-13 2391  ax-ext 2740
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1635  df-ex 1854  df-nf 1859  df-sb 2047  df-clab 2747  df-cleq 2753  df-clel 2756  df-if 4231
This theorem is referenced by:  dedth3h  4285  dedth4h  4286  dedth2v  4287  oawordeu  7806  oeoa  7848  unfilem3  8393  eluzadd  11928  eluzsub  11929  sqeqor  13192  binom2  13193  divalglem7  15344  divalg  15348  nmlno0  27980  ipassi  28026  sii  28039  ajfun  28046  ubth  28059  hvnegdi  28254  hvsubeq0  28255  normlem9at  28308  normsub0  28323  norm-ii  28325  norm-iii  28327  normsub  28330  normpyth  28332  norm3adifi  28340  normpar  28342  polid  28346  bcs  28368  shscl  28507  shslej  28569  shincl  28570  pjoc1  28623  pjoml  28625  pjoc2  28628  chincl  28688  chsscon3  28689  chlejb1  28701  chnle  28703  chdmm1  28714  spanun  28734  elspansn2  28756  h1datom  28771  cmbr3  28797  pjoml2  28800  pjoml3  28801  cmcm  28803  cmcm3  28804  lecm  28806  osum  28834  spansnj  28836  pjadji  28874  pjaddi  28875  pjsubi  28877  pjmuli  28878  pjch  28883  pj11  28903  pjnorm  28913  pjpyth  28914  pjnel  28915  hosubcl  28962  hoaddcom  28963  ho0sub  28986  honegsub  28988  eigre  29024  lnopeq0lem2  29195  lnopeq  29198  lnopunii  29201  lnophmi  29207  cvmd  29525  chrelat2  29559  cvexch  29563  mdsym  29601  kur14  31526  abs2sqle  31902  abs2sqlt  31903
  Copyright terms: Public domain W3C validator