Theorem pm5.32rd 577

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 576	. 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  630  pm5.71  1028  omord  8624  oeeui  8658  omxpenlem  9139  wemapwe  9766  fin23lem26  10394  1idpr  11098  repsdf2  14826  smueqlem  16536  tcphcph  25290  2sqreultlem  27509  2sqreunnltlem  27512  upgr2wlk  29704  upgrspthswlk  29774  isspthonpth  29785  iswwlksnx  29873  wwlksnextwrd  29930  rusgrnumwwlkl1  30001  isclwwlknx  30068  clwwlknwwlksnb  30087  clwwlknonel  30127  eupth2lem3lem6  30265  ordtconnlem1  33870  outsideofeu  36095  matunitlindf  37578  ftc1anclem6  37658  cvrval5  39372  cdleme0ex2N  40181  dihglb2  41299  fimgmcyc  42489  mrefg2  42663  rmydioph  42971  islssfg2  43028  fsovrfovd  43971  elfz2z  47230