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

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

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 397

This theorem is referenced by:  anbi1d  630  pm5.71  1026  omord  8567  oeeui  8601  omxpenlem  9072  wemapwe  9691  fin23lem26  10319  1idpr  11023  repsdf2  14727  smueqlem  16430  tcphcph  24753  2sqreultlem  26947  2sqreunnltlem  26950  upgr2wlk  28922  upgrspthswlk  28992  isspthonpth  29003  iswwlksnx  29091  wwlksnextwrd  29148  rusgrnumwwlkl1  29219  isclwwlknx  29286  clwwlknwwlksnb  29305  clwwlknonel  29345  eupth2lem3lem6  29483  ordtconnlem1  32899  outsideofeu  35098  matunitlindf  36481  ftc1anclem6  36561  cvrval5  38281  cdleme0ex2N  39090  dihglb2  40208  mrefg2  41435  rmydioph  41743  islssfg2  41803  fsovrfovd  42750  elfz2z  46013