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  8493  oeeui  8527  omxpenlem  9002  wemapwe  9612  fin23lem26  10238  1idpr  10942  repsdf2  14702  smueqlem  16419  tcphcph  25153  2sqreultlem  27374  2sqreunnltlem  27377  n0cutlt  28272  upgr2wlk  29630  upgrspthswlk  29701  isspthonpth  29712  iswwlksnx  29803  wwlksnextwrd  29860  rusgrnumwwlkl1  29931  isclwwlknx  29998  clwwlknwwlksnb  30017  clwwlknonel  30057  eupth2lem3lem6  30195  subsdrg  33250  ordtconnlem1  33893  outsideofeu  36107  matunitlindf  37600  ftc1anclem6  37680  cvrval5  39397  cdleme0ex2N  40206  dihglb2  41324  fimgmcyc  42510  mrefg2  42683  rmydioph  42990  islssfg2  43047  fsovrfovd  43985  elfz2z  47303