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 314	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  8399  oeeui  8433  omxpenlem  8860  wemapwe  9455  fin23lem26  10081  1idpr  10785  repsdf2  14491  smueqlem  16197  tcphcph  24401  2sqreultlem  26595  2sqreunnltlem  26598  upgr2wlk  28036  upgrspthswlk  28106  isspthonpth  28117  iswwlksnx  28205  wwlksnextwrd  28262  rusgrnumwwlkl1  28333  isclwwlknx  28400  clwwlknwwlksnb  28419  clwwlknonel  28459  eupth2lem3lem6  28597  ordtconnlem1  31874  outsideofeu  34433  matunitlindf  35775  ftc1anclem6  35855  cvrval5  37429  cdleme0ex2N  38238  dihglb2  39356  mrefg2  40529  rmydioph  40836  islssfg2  40896  fsovrfovd  41617  elfz2z  44807