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  339  imim21b  393  pm5.74da  802  sbiedvw  2089  sbiedw  2305  dvelimdf  2443  sbied  2497  2mosOLD  2639  cbvraldva2  3332  csbie2df  4437  dfiin2g  5032  oneqmini  6420  tfindsg  7863  findsg  7902  brecop  8831  dom2lem  9015  indpi  10941  nn0ind-raph  12708  cncls2  23265  ismbl2  25544  voliunlem3  25569  mdbr2  32226  dmdbr2  32233  mdsl2i  32252  mdsl2bi  32253  sgn3da  34388  wl-dral1d  37239  wl-equsald  37247  wl-equsaldv  37248  cvlsupr3  39055  cdleme32fva  40149  cdlemk33N  40621  cdlemk34  40622  ralbidar  44156  logic1  48214  tfis2d  48462
  Copyright terms: Public domain W3C validator