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

Theorem pm5.32rd 670
 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 669 . 2 (𝜑 → ((𝜓𝜒) ↔ (𝜓𝜃)))
3 ancom 465 . 2 ((𝜒𝜓) ↔ (𝜓𝜒))
4 ancom 465 . 2 ((𝜃𝜓) ↔ (𝜓𝜃))
52, 3, 43bitr4g 302 1 (𝜑 → ((𝜒𝜓) ↔ (𝜃𝜓)))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 195   ∧ wa 383 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 196  df-an 385 This theorem is referenced by:  anbi1d  737  pm5.71  973  omord  7535  oeeui  7569  omxpenlem  7946  wemapwe  8477  fin23lem26  9030  1idpr  9730  repsdf2  13376  smueqlem  15050  tchcph  22844  isusgra0  25876  is2wlk  26095  wwlkn0s  26233  wwlkextwrd  26256  clwwlkn2  26303  2pthwlkonot  26412  rusgranumwlkl1  26474  rusgra0edg  26482  eupath2lem3  26506  ordtconlem1  29298  outsideofeu  31408  matunitlindf  32577  ftc1anclem6  32660  cvrval5  33719  cdleme0ex2N  34529  dihglb2  35649  mrefg2  36288  rmydioph  36599  islssfg2  36659  fsovrfovd  37323  elfz2z  40352  upgr2wlk  40876  upgrspths1wlk  40944  isspthonpth-av  40955  iswwlksnx  41042  wwlksnextwrd  41103  rusgrnumwwlkl1  41172  isclwwlksnx  41197  eupth2lem3lem6  41401
 Copyright terms: Public domain W3C validator