Theorem pm5.32rd 589

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  anbi1d  643  pm5.71  1045  omord  8555  oeeui  8590  omxpenlem  9069  wemapwe  9669  fin23lem26  10320  1idpr  11025  repsdf2  14835  smueqlem  16566  tcphcph  25427  2sqreultlem  27642  2sqreunnltlem  27645  n0cutlt  28583  upgr2wlk  30050  upgrspthswlk  30127  isspthonpth  30138  iswwlksnx  30232  wwlksnextwrd  30289  rusgrnumwwlkl1  30363  isclwwlknx  30430  clwwlknwwlksnb  30449  clwwlknonel  30489  eupth2lem3lem6  30631  subsdrg  33659  ordtconnlem1  34354  outsideofeu  36636  matunitlindf  38302  ftc1anclem6  38382  cvrval5  40222  cdleme0ex2N  41031  dihglb2  42149  fimgmcyc  43335  mrefg2  43471  rmydioph  43774  islssfg2  43831  fsovrfovd  44768  elfz2z  48085