Theorem pm5.32rd 577

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

Syntax hints:   → wi 4   ↔ wb 205   ∧ 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 206  df-an 396

This theorem is referenced by:  anbi1d  629  pm5.71  1024  omord  8361  oeeui  8395  omxpenlem  8813  wemapwe  9385  fin23lem26  10012  1idpr  10716  repsdf2  14419  smueqlem  16125  tcphcph  24306  2sqreultlem  26500  2sqreunnltlem  26503  upgr2wlk  27938  upgrspthswlk  28007  isspthonpth  28018  iswwlksnx  28106  wwlksnextwrd  28163  rusgrnumwwlkl1  28234  isclwwlknx  28301  clwwlknwwlksnb  28320  clwwlknonel  28360  eupth2lem3lem6  28498  ordtconnlem1  31776  outsideofeu  34360  matunitlindf  35702  ftc1anclem6  35782  cvrval5  37356  cdleme0ex2N  38165  dihglb2  39283  mrefg2  40445  rmydioph  40752  islssfg2  40812  fsovrfovd  41506  elfz2z  44695