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 578
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 577 . 2 (𝜑 → ((𝜓𝜒) ↔ (𝜓𝜃)))
3 ancom 461 . 2 ((𝜒𝜓) ↔ (𝜓𝜒))
4 ancom 461 . 2 ((𝜃𝜓) ↔ (𝜓𝜃))
52, 3, 43bitr4g 315 1 (𝜑 → ((𝜒𝜓) ↔ (𝜃𝜓)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 207  wa 396
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 208  df-an 397
This theorem is referenced by:  anbi1d  629  pm5.71  1021  omord  8183  oeeui  8217  omxpenlem  8606  wemapwe  9148  fin23lem26  9735  1idpr  10439  repsdf2  14128  smueqlem  15827  tcphcph  23767  2sqreultlem  25950  2sqreunnltlem  25953  upgr2wlk  27377  upgrspthswlk  27446  isspthonpth  27457  iswwlksnx  27545  wwlksnextwrd  27602  rusgrnumwwlkl1  27674  isclwwlknx  27741  clwwlknwwlksnb  27761  clwwlknonel  27801  eupth2lem3lem6  27939  ordtconnlem1  31066  outsideofeu  33489  matunitlindf  34771  ftc1anclem6  34853  cvrval5  36431  cdleme0ex2N  37240  dihglb2  38358  mrefg2  39182  rmydioph  39489  islssfg2  39549  fsovrfovd  40233  elfz2z  43392
  Copyright terms: Public domain W3C validator