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  8585  oeeui  8619  omxpenlem  9092  wemapwe  9716  fin23lem26  10344  1idpr  11048  repsdf2  14801  smueqlem  16514  tcphcph  25194  2sqreultlem  27415  2sqreunnltlem  27418  n0cutlt  28306  upgr2wlk  29653  upgrspthswlk  29725  isspthonpth  29736  iswwlksnx  29827  wwlksnextwrd  29884  rusgrnumwwlkl1  29955  isclwwlknx  30022  clwwlknwwlksnb  30041  clwwlknonel  30081  eupth2lem3lem6  30219  subsdrg  33297  ordtconnlem1  33960  outsideofeu  36154  matunitlindf  37647  ftc1anclem6  37727  cvrval5  39439  cdleme0ex2N  40248  dihglb2  41366  fimgmcyc  42524  mrefg2  42697  rmydioph  43005  islssfg2  43062  fsovrfovd  44000  elfz2z  47311