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

Theorem pm5.74d 276
 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 273 . 2 ((𝜓 → (𝜒𝜃)) ↔ ((𝜓𝜒) ↔ (𝜓𝜃)))
31, 2sylib 221 1 (𝜑 → ((𝜓𝜒) ↔ (𝜓𝜃)))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 209 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 210 This theorem is referenced by:  imbi2d  344  imim21b  398  pm5.74da  803  sbiedvw  2101  sbiedw  2323  sbiedwOLD  2324  cbval2vOLD  2353  cbval2OLD  2422  dvelimdf  2460  sbied  2522  sbiedALT  2590  2mos  2711  cbvraldva2  3403  cbvrexdva2OLD  3405  csbie2df  4348  dfiin2g  4919  oneqmini  6210  tfindsg  7557  findsg  7592  brecop  8375  dom2lem  8534  indpi  10320  nn0ind-raph  12072  cncls2  21885  ismbl2  24138  voliunlem3  24163  mdbr2  30086  dmdbr2  30093  mdsl2i  30112  mdsl2bi  30113  sgn3da  31921  wl-dral1d  34952  wl-equsald  34960  cvlsupr3  36656  cdleme32fva  37749  cdlemk33N  38221  cdlemk34  38222  ralbidar  41164  tfis2d  45224
 Copyright terms: Public domain W3C validator