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  632  pm5.71  1030  omord  8503  oeeui  8538  omxpenlem  9016  wemapwe  9618  fin23lem26  10247  1idpr  10952  repsdf2  14740  smueqlem  16459  tcphcph  25204  2sqreultlem  27410  2sqreunnltlem  27413  n0cutlt  28351  upgr2wlk  29735  upgrspthswlk  29806  isspthonpth  29817  iswwlksnx  29908  wwlksnextwrd  29965  rusgrnumwwlkl1  30039  isclwwlknx  30106  clwwlknwwlksnb  30125  clwwlknonel  30165  eupth2lem3lem6  30303  subsdrg  33359  ordtconnlem1  34068  outsideofeu  36313  matunitlindf  37939  ftc1anclem6  38019  cvrval5  39861  cdleme0ex2N  40670  dihglb2  41788  fimgmcyc  42979  mrefg2  43139  rmydioph  43442  islssfg2  43499  fsovrfovd  44436  elfz2z  47763