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

Theorem pm5.32rd 579
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 578 . 2 (𝜑 → ((𝜓𝜒) ↔ (𝜓𝜃)))
3 ancom 462 . 2 ((𝜒𝜓) ↔ (𝜓𝜒))
4 ancom 462 . 2 ((𝜃𝜓) ↔ (𝜓𝜃))
52, 3, 43bitr4g 314 1 (𝜑 → ((𝜒𝜓) ↔ (𝜃𝜓)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 397
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  df-an 398
This theorem is referenced by:  anbi1d  631  pm5.71  1027  omord  8519  oeeui  8553  omxpenlem  9023  wemapwe  9641  fin23lem26  10269  1idpr  10973  repsdf2  14675  smueqlem  16378  tcphcph  24624  2sqreultlem  26818  2sqreunnltlem  26821  upgr2wlk  28665  upgrspthswlk  28735  isspthonpth  28746  iswwlksnx  28834  wwlksnextwrd  28891  rusgrnumwwlkl1  28962  isclwwlknx  29029  clwwlknwwlksnb  29048  clwwlknonel  29088  eupth2lem3lem6  29226  ordtconnlem1  32569  outsideofeu  34769  matunitlindf  36126  ftc1anclem6  36206  cvrval5  37928  cdleme0ex2N  38737  dihglb2  39855  mrefg2  41077  rmydioph  41385  islssfg2  41445  fsovrfovd  42373  elfz2z  45637
  Copyright terms: Public domain W3C validator