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  1025  omord  8470  oeeui  8504  omxpenlem  8938  wemapwe  9554  fin23lem26  10182  1idpr  10886  repsdf2  14589  smueqlem  16296  tcphcph  24507  2sqreultlem  26701  2sqreunnltlem  26704  upgr2wlk  28324  upgrspthswlk  28394  isspthonpth  28405  iswwlksnx  28493  wwlksnextwrd  28550  rusgrnumwwlkl1  28621  isclwwlknx  28688  clwwlknwwlksnb  28707  clwwlknonel  28747  eupth2lem3lem6  28885  ordtconnlem1  32172  outsideofeu  34529  matunitlindf  35888  ftc1anclem6  35968  cvrval5  37691  cdleme0ex2N  38500  dihglb2  39618  mrefg2  40799  rmydioph  41107  islssfg2  41167  fsovrfovd  41946  elfz2z  45166