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  1043  omord  8549  oeeui  8584  omxpenlem  9062  wemapwe  9662  fin23lem26  10305  1idpr  11010  repsdf2  14811  smueqlem  16544  tcphcph  25361  2sqreultlem  27573  2sqreunnltlem  27576  n0cutlt  28514  upgr2wlk  29953  upgrspthswlk  30024  isspthonpth  30035  iswwlksnx  30126  wwlksnextwrd  30183  rusgrnumwwlkl1  30257  isclwwlknx  30324  clwwlknwwlksnb  30343  clwwlknonel  30383  eupth2lem3lem6  30521  subsdrg  33558  ordtconnlem1  34255  outsideofeu  36518  matunitlindf  38152  ftc1anclem6  38232  cvrval5  40074  cdleme0ex2N  40883  dihglb2  42001  fimgmcyc  43187  mrefg2  43323  rmydioph  43626  islssfg2  43683  fsovrfovd  44620  elfz2z  47934