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  8569  oeeui  8604  omxpenlem  9090  wemapwe  9691  fin23lem26  10396  1idpr  11107  repsdf2  14922  smueqlem  16653  matunitlindf  22989  tcphcph  25551  2sqreultlem  27767  2sqreunnltlem  27770  n0cutlt  28738  upgr2wlk  30240  upgrspthswlk  30317  isspthonpth  30328  iswwlksnx  30422  wwlksnextwrd  30479  rusgrnumwwlkl1  30553  isclwwlknx  30620  clwwlknwwlksnb  30639  clwwlknonel  30679  eupth2lem3lem6  30827  subsdrg  33853  ordtconnlem1  34549  outsideofeu  36876  ftc1anclem6  38596  cvrval5  40452  cdleme0ex2N  41261  dihglb2  42379  fimgmcyc  43578  mrefg2  43697  rmydioph  44000  islssfg2  44057  fsovrfovd  44994  elfz2z  48354