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  8496  oeeui  8531  omxpenlem  9009  wemapwe  9609  fin23lem26  10238  1idpr  10943  repsdf2  14731  smueqlem  16450  tcphcph  25214  2sqreultlem  27424  2sqreunnltlem  27427  n0cutlt  28365  upgr2wlk  29750  upgrspthswlk  29821  isspthonpth  29832  iswwlksnx  29923  wwlksnextwrd  29980  rusgrnumwwlkl1  30054  isclwwlknx  30121  clwwlknwwlksnb  30140  clwwlknonel  30180  eupth2lem3lem6  30318  subsdrg  33374  ordtconnlem1  34084  outsideofeu  36329  matunitlindf  37953  ftc1anclem6  38033  cvrval5  39875  cdleme0ex2N  40684  dihglb2  41802  fimgmcyc  42993  mrefg2  43153  rmydioph  43460  islssfg2  43517  fsovrfovd  44454  elfz2z  47775