Theorem pm5.32rd 588

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

Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 400

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 210  df-an 401

This theorem is referenced by:  anbi1d  642  pm5.71  1045  omord  8549  oeeui  8584  omxpenlem  9062  wemapwe  9662  fin23lem26  10304  1idpr  11009  repsdf2  14811  smueqlem  16543  tcphcph  25396  2sqreultlem  27611  2sqreunnltlem  27614  n0cutlt  28552  upgr2wlk  30016  upgrspthswlk  30087  isspthonpth  30098  iswwlksnx  30189  wwlksnextwrd  30246  rusgrnumwwlkl1  30320  isclwwlknx  30387  clwwlknwwlksnb  30406  clwwlknonel  30446  eupth2lem3lem6  30584  subsdrg  33619  ordtconnlem1  34314  outsideofeu  36623  matunitlindf  38269  ftc1anclem6  38349  cvrval5  40189  cdleme0ex2N  40998  dihglb2  42116  fimgmcyc  43302  mrefg2  43438  rmydioph  43741  islssfg2  43798  fsovrfovd  44735  elfz2z  48052