Theorem pm5.32rd 672

Description: Distribution of implication over biconditional (deduction rule). (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 671	. 2 ⊢ (𝜑 → ((𝜓 ∧ 𝜒) ↔ (𝜓 ∧ 𝜃)))
3		ancom 466	. 2 ⊢ ((𝜒 ∧ 𝜓) ↔ (𝜓 ∧ 𝜒))
4		ancom 466	. 2 ⊢ ((𝜃 ∧ 𝜓) ↔ (𝜓 ∧ 𝜃))
5	2, 3, 4	3bitr4g 303	1 ⊢ (𝜑 → ((𝜒 ∧ 𝜓) ↔ (𝜃 ∧ 𝜓)))

Syntax hints:   → wi 4   ↔ wb 196   ∧ wa 384

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 197  df-an 386

This theorem is referenced by:  anbi1d  741  pm5.71  977  omord  7648  oeeui  7682  omxpenlem  8061  wemapwe  8594  fin23lem26  9147  1idpr  9851  repsdf2  13525  smueqlem  15212  tchcph  23036  upgr2wlk  26564  upgrspthswlk  26634  isspthonpth  26645  iswwlksnx  26731  wwlksnextwrd  26792  rusgrnumwwlkl1  26863  isclwwlksnx  26889  eupth2lem3lem6  27093  ordtconnlem1  29970  eqfunresadj  31659  outsideofeu  32238  matunitlindf  33407  ftc1anclem6  33490  cvrval5  34701  cdleme0ex2N  35511  dihglb2  36631  mrefg2  37270  rmydioph  37581  islssfg2  37641  fsovrfovd  38303  elfz2z  41325