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

Theorem pm5.32rd 581
 Description: Distribution of implication over biconditional (deduction form). (Contributed by NM, 25-Dec-2004.)
Hypothesis
Ref Expression
pm5.32d.1 (𝜑 → (𝜓 → (𝜒𝜃)))
Assertion
Ref Expression
pm5.32rd (𝜑 → ((𝜒𝜓) ↔ (𝜃𝜓)))

Proof of Theorem pm5.32rd
StepHypRef Expression
1 pm5.32d.1 . . 3 (𝜑 → (𝜓 → (𝜒𝜃)))
21pm5.32d 580 . 2 (𝜑 → ((𝜓𝜒) ↔ (𝜓𝜃)))
3 ancom 464 . 2 ((𝜒𝜓) ↔ (𝜓𝜒))
4 ancom 464 . 2 ((𝜃𝜓) ↔ (𝜓𝜃))
52, 3, 43bitr4g 317 1 (𝜑 → ((𝜒𝜓) ↔ (𝜃𝜓)))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 399 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  df-an 400 This theorem is referenced by:  anbi1d  632  pm5.71  1025  omord  8179  oeeui  8213  omxpenlem  8603  wemapwe  9146  fin23lem26  9738  1idpr  10442  repsdf2  14133  smueqlem  15831  tcphcph  23848  2sqreultlem  26038  2sqreunnltlem  26041  upgr2wlk  27465  upgrspthswlk  27534  isspthonpth  27545  iswwlksnx  27633  wwlksnextwrd  27690  rusgrnumwwlkl1  27761  isclwwlknx  27828  clwwlknwwlksnb  27847  clwwlknonel  27887  eupth2lem3lem6  28025  ordtconnlem1  31289  outsideofeu  33717  matunitlindf  35071  ftc1anclem6  35151  cvrval5  36727  cdleme0ex2N  37536  dihglb2  38654  mrefg2  39663  rmydioph  39970  islssfg2  40030  fsovrfovd  40725  elfz2z  43887
 Copyright terms: Public domain W3C validator