Theorem pm5.32rd 567

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

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

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 383

This theorem is referenced by:  anbi1d  615  pm5.71  1014  omord  7806  oeeui  7840  omxpenlem  8221  wemapwe  8762  fin23lem26  9353  1idpr  10057  repsdf2  13734  smueqlem  15420  tchcph  23255  upgr2wlk  26799  upgrspthswlk  26869  isspthonpth  26880  iswwlksnx  26968  wwlksnextwrd  27041  rusgrnumwwlkl1  27117  isclwwlknx  27191  clwwlknwwlksnb  27212  clwwlknonel  27269  eupth2lem3lem6  27413  ordtconnlem1  30310  eqfunresadj  31997  outsideofeu  32575  matunitlindf  33740  ftc1anclem6  33822  cvrval5  35224  cdleme0ex2N  36034  dihglb2  37152  mrefg2  37796  rmydioph  38107  islssfg2  38167  fsovrfovd  38829  elfz2z  41850