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  8492  oeeui  8526  omxpenlem  9002  wemapwe  9598  fin23lem26  10227  1idpr  10931  repsdf2  14692  smueqlem  16408  tcphcph  25184  2sqreultlem  27405  2sqreunnltlem  27408  n0cutlt  28305  upgr2wlk  29666  upgrspthswlk  29737  isspthonpth  29748  iswwlksnx  29839  wwlksnextwrd  29896  rusgrnumwwlkl1  29970  isclwwlknx  30037  clwwlknwwlksnb  30056  clwwlknonel  30096  eupth2lem3lem6  30234  subsdrg  33308  ordtconnlem1  34009  outsideofeu  36247  matunitlindf  37731  ftc1anclem6  37811  cvrval5  39587  cdleme0ex2N  40396  dihglb2  41514  fimgmcyc  42704  mrefg2  42864  rmydioph  43171  islssfg2  43228  fsovrfovd  44166  elfz2z  47477