Theorem pm5.32rd 589

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  anbi1d  643  pm5.71  1045  omord  8580  oeeui  8615  omxpenlem  9101  wemapwe  9702  fin23lem26  10407  1idpr  11118  repsdf2  14934  smueqlem  16666  matunitlindf  23002  tcphcph  25564  2sqreultlem  27780  2sqreunnltlem  27783  n0cutlt  28751  upgr2wlk  30253  upgrspthswlk  30330  isspthonpth  30341  iswwlksnx  30435  wwlksnextwrd  30492  rusgrnumwwlkl1  30566  isclwwlknx  30633  clwwlknwwlksnb  30652  clwwlknonel  30692  eupth2lem3lem6  30840  subsdrg  33907  ordtconnlem1  34603  outsideofeu  36989  ftc1anclem6  38710  cvrval5  40566  cdleme0ex2N  41375  dihglb2  42493  fimgmcyc  43692  mrefg2  43812  rmydioph  44115  islssfg2  44167  fsovrfovd  45103  elfz2z  48479