Theorem pm5.32rd 580

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

Syntax hints:   → wi 4   ↔ wb 208   ∧ wa 398

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 209  df-an 399

This theorem is referenced by:  anbi1d  631  pm5.71  1024  omord  8194  oeeui  8228  omxpenlem  8618  wemapwe  9160  fin23lem26  9747  1idpr  10451  repsdf2  14140  smueqlem  15839  tcphcph  23840  2sqreultlem  26023  2sqreunnltlem  26026  upgr2wlk  27450  upgrspthswlk  27519  isspthonpth  27530  iswwlksnx  27618  wwlksnextwrd  27675  rusgrnumwwlkl1  27747  isclwwlknx  27814  clwwlknwwlksnb  27834  clwwlknonel  27874  eupth2lem3lem6  28012  ordtconnlem1  31167  outsideofeu  33592  matunitlindf  34905  ftc1anclem6  34987  cvrval5  36566  cdleme0ex2N  37375  dihglb2  38493  mrefg2  39353  rmydioph  39660  islssfg2  39720  fsovrfovd  40404  elfz2z  43564