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  8483  oeeui  8517  omxpenlem  8991  wemapwe  9587  fin23lem26  10216  1idpr  10920  repsdf2  14685  smueqlem  16401  tcphcph  25164  2sqreultlem  27385  2sqreunnltlem  27388  n0cutlt  28285  upgr2wlk  29645  upgrspthswlk  29716  isspthonpth  29727  iswwlksnx  29818  wwlksnextwrd  29875  rusgrnumwwlkl1  29949  isclwwlknx  30016  clwwlknwwlksnb  30035  clwwlknonel  30075  eupth2lem3lem6  30213  subsdrg  33264  ordtconnlem1  33937  outsideofeu  36175  matunitlindf  37668  ftc1anclem6  37748  cvrval5  39524  cdleme0ex2N  40333  dihglb2  41451  fimgmcyc  42637  mrefg2  42810  rmydioph  43117  islssfg2  43174  fsovrfovd  44112  elfz2z  47425