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

Theorem pm5.32rd 567
 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 566 . 2 (𝜑 → ((𝜓𝜒) ↔ (𝜓𝜃)))
3 ancom 448 . 2 ((𝜒𝜓) ↔ (𝜓𝜒))
4 ancom 448 . 2 ((𝜃𝜓) ↔ (𝜓𝜃))
52, 3, 43bitr4g 303 1 (𝜑 → ((𝜒𝜓) ↔ (𝜃𝜓)))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 196   ∧ wa 382 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 383 This theorem is referenced by:  anbi1d  615  pm5.71  1014  omord  7806  oeeui  7840  omxpenlem  8221  wemapwe  8762  fin23lem26  9353  1idpr  10057  repsdf2  13734  smueqlem  15420  tchcph  23255  upgr2wlk  26799  upgrspthswlk  26869  isspthonpth  26880  iswwlksnx  26968  wwlksnextwrd  27041  rusgrnumwwlkl1  27117  isclwwlknx  27191  clwwlknwwlksnb  27212  clwwlknonel  27269  eupth2lem3lem6  27413  ordtconnlem1  30310  eqfunresadj  31997  outsideofeu  32575  matunitlindf  33740  ftc1anclem6  33822  cvrval5  35224  cdleme0ex2N  36034  dihglb2  37152  mrefg2  37796  rmydioph  38107  islssfg2  38167  fsovrfovd  38829  elfz2z  41850
 Copyright terms: Public domain W3C validator