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

Step	Hyp	Ref	Expression
1		pm5.32d.1	. . 3 ⊢ (𝜑 → (𝜓 → (𝜒 ↔ 𝜃)))
2	1	pm5.32d 577	. 2 ⊢ (𝜑 → ((𝜓 ∧ 𝜒) ↔ (𝜓 ∧ 𝜃)))
3		ancom 460	. 2 ⊢ ((𝜒 ∧ 𝜓) ↔ (𝜓 ∧ 𝜒))
4		ancom 460	. 2 ⊢ ((𝜃 ∧ 𝜓) ↔ (𝜓 ∧ 𝜃))
5	2, 3, 4	3bitr4g 314	1 ⊢ (𝜑 → ((𝜒 ∧ 𝜓) ↔ (𝜃 ∧ 𝜓)))

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395

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 207  df-an 396

This theorem is referenced by:  anbi1d  631  pm5.71  1029  omord  8532  oeeui  8566  omxpenlem  9042  wemapwe  9650  fin23lem26  10278  1idpr  10982  repsdf2  14743  smueqlem  16460  tcphcph  25137  2sqreultlem  27358  2sqreunnltlem  27361  n0cutlt  28249  upgr2wlk  29596  upgrspthswlk  29668  isspthonpth  29679  iswwlksnx  29770  wwlksnextwrd  29827  rusgrnumwwlkl1  29898  isclwwlknx  29965  clwwlknwwlksnb  29984  clwwlknonel  30024  eupth2lem3lem6  30162  subsdrg  33248  ordtconnlem1  33914  outsideofeu  36119  matunitlindf  37612  ftc1anclem6  37692  cvrval5  39409  cdleme0ex2N  40218  dihglb2  41336  fimgmcyc  42522  mrefg2  42695  rmydioph  43003  islssfg2  43060  fsovrfovd  43998  elfz2z  47316