Theorem pm5.32rd 578

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

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395

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 207  df-an 396

This theorem is referenced by:  anbi1d  631  pm5.71  1029  omord  8478  oeeui  8512  omxpenlem  8986  wemapwe  9582  fin23lem26  10211  1idpr  10915  repsdf2  14680  smueqlem  16396  tcphcph  25159  2sqreultlem  27380  2sqreunnltlem  27383  n0cutlt  28280  upgr2wlk  29640  upgrspthswlk  29711  isspthonpth  29722  iswwlksnx  29813  wwlksnextwrd  29870  rusgrnumwwlkl1  29941  isclwwlknx  30008  clwwlknwwlksnb  30027  clwwlknonel  30067  eupth2lem3lem6  30205  subsdrg  33256  ordtconnlem1  33929  outsideofeu  36165  matunitlindf  37658  ftc1anclem6  37738  cvrval5  39454  cdleme0ex2N  40263  dihglb2  41381  fimgmcyc  42567  mrefg2  42740  rmydioph  43047  islssfg2  43104  fsovrfovd  44042  elfz2z  47346