Theorem pm5.32rd 578

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

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395

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 207  df-an 396

This theorem is referenced by:  anbi1d  631  pm5.71  1029  omord  8495  oeeui  8530  omxpenlem  9006  wemapwe  9606  fin23lem26  10235  1idpr  10940  repsdf2  14701  smueqlem  16417  tcphcph  25193  2sqreultlem  27414  2sqreunnltlem  27417  n0cutlt  28355  upgr2wlk  29740  upgrspthswlk  29811  isspthonpth  29822  iswwlksnx  29913  wwlksnextwrd  29970  rusgrnumwwlkl1  30044  isclwwlknx  30111  clwwlknwwlksnb  30130  clwwlknonel  30170  eupth2lem3lem6  30308  subsdrg  33380  ordtconnlem1  34081  outsideofeu  36325  matunitlindf  37819  ftc1anclem6  37899  cvrval5  39675  cdleme0ex2N  40484  dihglb2  41602  fimgmcyc  42789  mrefg2  42949  rmydioph  43256  islssfg2  43313  fsovrfovd  44250  elfz2z  47561