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  8558  oeeui  8593  omxpenlem  9079  wemapwe  9679  fin23lem26  10330  1idpr  11041  repsdf2  14852  smueqlem  16583  matunitlindf  22906  tcphcph  25468  2sqreultlem  27686  2sqreunnltlem  27689  n0cutlt  28627  upgr2wlk  30129  upgrspthswlk  30206  isspthonpth  30217  iswwlksnx  30311  wwlksnextwrd  30368  rusgrnumwwlkl1  30442  isclwwlknx  30509  clwwlknwwlksnb  30528  clwwlknonel  30568  eupth2lem3lem6  30716  subsdrg  33742  ordtconnlem1  34437  outsideofeu  36714  ftc1anclem6  38450  cvrval5  40291  cdleme0ex2N  41100  dihglb2  42218  fimgmcyc  43419  mrefg2  43555  rmydioph  43858  islssfg2  43915  fsovrfovd  44852  elfz2z  48206