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  1030  omord  8606  oeeui  8640  omxpenlem  9113  wemapwe  9737  fin23lem26  10365  1idpr  11069  repsdf2  14816  smueqlem  16527  tcphcph  25271  2sqreultlem  27491  2sqreunnltlem  27494  upgr2wlk  29686  upgrspthswlk  29758  isspthonpth  29769  iswwlksnx  29860  wwlksnextwrd  29917  rusgrnumwwlkl1  29988  isclwwlknx  30055  clwwlknwwlksnb  30074  clwwlknonel  30114  eupth2lem3lem6  30252  ordtconnlem1  33923  outsideofeu  36132  matunitlindf  37625  ftc1anclem6  37705  cvrval5  39417  cdleme0ex2N  40226  dihglb2  41344  fimgmcyc  42544  mrefg2  42718  rmydioph  43026  islssfg2  43083  fsovrfovd  44022  elfz2z  47327