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  8535  oeeui  8569  omxpenlem  9047  wemapwe  9657  fin23lem26  10285  1idpr  10989  repsdf2  14750  smueqlem  16467  tcphcph  25144  2sqreultlem  27365  2sqreunnltlem  27368  n0cutlt  28256  upgr2wlk  29603  upgrspthswlk  29675  isspthonpth  29686  iswwlksnx  29777  wwlksnextwrd  29834  rusgrnumwwlkl1  29905  isclwwlknx  29972  clwwlknwwlksnb  29991  clwwlknonel  30031  eupth2lem3lem6  30169  subsdrg  33255  ordtconnlem1  33921  outsideofeu  36126  matunitlindf  37619  ftc1anclem6  37699  cvrval5  39416  cdleme0ex2N  40225  dihglb2  41343  fimgmcyc  42529  mrefg2  42702  rmydioph  43010  islssfg2  43067  fsovrfovd  44005  elfz2z  47320