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  9076  wemapwe  9676  fin23lem26  10327  1idpr  11038  repsdf2  14849  smueqlem  16580  matunitlindf  22903  tcphcph  25465  2sqreultlem  27683  2sqreunnltlem  27686  n0cutlt  28624  upgr2wlk  30126  upgrspthswlk  30203  isspthonpth  30214  iswwlksnx  30308  wwlksnextwrd  30365  rusgrnumwwlkl1  30439  isclwwlknx  30506  clwwlknwwlksnb  30525  clwwlknonel  30565  eupth2lem3lem6  30713  subsdrg  33739  ordtconnlem1  34434  outsideofeu  36711  ftc1anclem6  38447  cvrval5  40288  cdleme0ex2N  41097  dihglb2  42215  fimgmcyc  43416  mrefg2  43552  rmydioph  43855  islssfg2  43912  fsovrfovd  44849  elfz2z  48203