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

Theorem pm5.32rd 671
 Description: Distribution of implication over biconditional (deduction rule). (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 670 . 2 (𝜑 → ((𝜓𝜒) ↔ (𝜓𝜃)))
3 ancom 466 . 2 ((𝜒𝜓) ↔ (𝜓𝜒))
4 ancom 466 . 2 ((𝜃𝜓) ↔ (𝜓𝜃))
52, 3, 43bitr4g 303 1 (𝜑 → ((𝜒𝜓) ↔ (𝜃𝜓)))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 196   ∧ wa 384 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 197  df-an 386 This theorem is referenced by:  anbi1d  740  pm5.71  976  omord  7593  oeeui  7627  omxpenlem  8005  wemapwe  8538  fin23lem26  9091  1idpr  9795  repsdf2  13462  smueqlem  15136  tchcph  22944  upgr2wlk  26433  upgrspthswlk  26503  isspthonpth  26514  iswwlksnx  26600  wwlksnextwrd  26661  rusgrnumwwlkl1  26730  isclwwlksnx  26756  eupth2lem3lem6  26959  ordtconnlem1  29749  outsideofeu  31877  matunitlindf  33036  ftc1anclem6  33119  cvrval5  34178  cdleme0ex2N  34988  dihglb2  36108  mrefg2  36747  rmydioph  37058  islssfg2  37118  fsovrfovd  37782  elfz2z  40619
 Copyright terms: Public domain W3C validator