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

Theorem pm5.74d 272
Description: Distribution of implication over biconditional (deduction form). (Contributed by NM, 21-Mar-1996.)
Hypothesis
Ref Expression
pm5.74d.1 (𝜑 → (𝜓 → (𝜒𝜃)))
Assertion
Ref Expression
pm5.74d (𝜑 → ((𝜓𝜒) ↔ (𝜓𝜃)))

Proof of Theorem pm5.74d
StepHypRef Expression
1 pm5.74d.1 . 2 (𝜑 → (𝜓 → (𝜒𝜃)))
2 pm5.74 269 . 2 ((𝜓 → (𝜒𝜃)) ↔ ((𝜓𝜒) ↔ (𝜓𝜃)))
31, 2sylib 217 1 (𝜑 → ((𝜓𝜒) ↔ (𝜓𝜃)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem depends on definitions:  df-bi 206
This theorem is referenced by:  imbi2d  340  imim21b  395  pm5.74da  802  sbiedvw  2096  sbiedw  2310  dvelimdf  2448  sbied  2506  2mos  2650  cbvraldva2  3321  csbie2df  4398  dfiin2g  4990  oneqmini  6367  tfindsg  7789  findsg  7828  brecop  8707  dom2lem  8890  indpi  10801  nn0ind-raph  12561  cncls2  22576  ismbl2  24843  voliunlem3  24868  mdbr2  31067  dmdbr2  31074  mdsl2i  31093  mdsl2bi  31094  sgn3da  32953  wl-dral1d  35928  wl-equsald  35936  cvlsupr3  37744  cdleme32fva  38838  cdlemk33N  39310  cdlemk34  39311  ralbidar  42636  logic1  46777  tfis2d  47026
  Copyright terms: Public domain W3C validator