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 265
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 262 . 2 ((𝜓 → (𝜒𝜃)) ↔ ((𝜓𝜒) ↔ (𝜓𝜃)))
31, 2sylib 210 1 (𝜑 → ((𝜓𝜒) ↔ (𝜓𝜃)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 198
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 199
This theorem is referenced by:  imbi2d  333  imim21b  386  pm5.74da  791  cbval2OLD  2344  dvelimdf  2383  sbied  2467  sbiedALT  2538  2mos  2675  cbvraldva2  3381  cbvrexdva2OLD  3383  dfiin2g  4821  oneqmini  6074  tfindsg  7385  findsg  7418  brecop  8182  dom2lem  8338  indpi  10119  nn0ind-raph  11888  cncls2  21575  ismbl2  23821  voliunlem3  23846  mdbr2  29844  dmdbr2  29851  mdsl2i  29870  mdsl2bi  29871  sgn3da  31402  bj-cbval2v  33522  wl-dral1d  34149  wl-equsald  34157  cvlsupr3  35873  cdleme32fva  36966  cdlemk33N  37438  cdlemk34  37439  ralbidar  40140  tfis2d  44090
  Copyright terms: Public domain W3C validator