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  8604  oeeui  8638  omxpenlem  9111  wemapwe  9734  fin23lem26  10362  1idpr  11066  repsdf2  14812  smueqlem  16523  tcphcph  25284  2sqreultlem  27505  2sqreunnltlem  27508  upgr2wlk  29700  upgrspthswlk  29770  isspthonpth  29781  iswwlksnx  29869  wwlksnextwrd  29926  rusgrnumwwlkl1  29997  isclwwlknx  30064  clwwlknwwlksnb  30083  clwwlknonel  30123  eupth2lem3lem6  30261  ordtconnlem1  33884  outsideofeu  36112  matunitlindf  37604  ftc1anclem6  37684  cvrval5  39397  cdleme0ex2N  40206  dihglb2  41324  fimgmcyc  42520  mrefg2  42694  rmydioph  43002  islssfg2  43059  fsovrfovd  43998  elfz2z  47264