Theorem pm5.32rd 576

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 575	. 2 ⊢ (𝜑 → ((𝜓 ∧ 𝜒) ↔ (𝜓 ∧ 𝜃)))
3		ancom 459	. 2 ⊢ ((𝜒 ∧ 𝜓) ↔ (𝜓 ∧ 𝜒))
4		ancom 459	. 2 ⊢ ((𝜃 ∧ 𝜓) ↔ (𝜓 ∧ 𝜃))
5	2, 3, 4	3bitr4g 313	1 ⊢ (𝜑 → ((𝜒 ∧ 𝜓) ↔ (𝜃 ∧ 𝜓)))

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 394

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 206  df-an 395

This theorem is referenced by:  anbi1d  628  pm5.71  1024  omord  8570  oeeui  8604  omxpenlem  9075  wemapwe  9694  fin23lem26  10322  1idpr  11026  repsdf2  14732  smueqlem  16435  tcphcph  24985  2sqreultlem  27186  2sqreunnltlem  27189  upgr2wlk  29192  upgrspthswlk  29262  isspthonpth  29273  iswwlksnx  29361  wwlksnextwrd  29418  rusgrnumwwlkl1  29489  isclwwlknx  29556  clwwlknwwlksnb  29575  clwwlknonel  29615  eupth2lem3lem6  29753  ordtconnlem1  33202  outsideofeu  35407  matunitlindf  36789  ftc1anclem6  36869  cvrval5  38589  cdleme0ex2N  39398  dihglb2  40516  mrefg2  41747  rmydioph  42055  islssfg2  42115  fsovrfovd  43062  elfz2z  46321