Theorem pm5.32rd 581

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

Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 399

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 210  df-an 400

This theorem is referenced by:  anbi1d  633  pm5.71  1028  omord  8296  oeeui  8330  omxpenlem  8746  wemapwe  9312  fin23lem26  9939  1idpr  10643  repsdf2  14343  smueqlem  16049  tcphcph  24134  2sqreultlem  26328  2sqreunnltlem  26331  upgr2wlk  27756  upgrspthswlk  27825  isspthonpth  27836  iswwlksnx  27924  wwlksnextwrd  27981  rusgrnumwwlkl1  28052  isclwwlknx  28119  clwwlknwwlksnb  28138  clwwlknonel  28178  eupth2lem3lem6  28316  ordtconnlem1  31588  outsideofeu  34170  matunitlindf  35512  ftc1anclem6  35592  cvrval5  37166  cdleme0ex2N  37975  dihglb2  39093  mrefg2  40232  rmydioph  40539  islssfg2  40599  fsovrfovd  41294  elfz2z  44480