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  632  pm5.71  1030  omord  8505  oeeui  8540  omxpenlem  9018  wemapwe  9618  fin23lem26  10247  1idpr  10952  repsdf2  14713  smueqlem  16429  tcphcph  25205  2sqreultlem  27426  2sqreunnltlem  27429  n0cutlt  28367  upgr2wlk  29752  upgrspthswlk  29823  isspthonpth  29834  iswwlksnx  29925  wwlksnextwrd  29982  rusgrnumwwlkl1  30056  isclwwlknx  30123  clwwlknwwlksnb  30142  clwwlknonel  30182  eupth2lem3lem6  30320  subsdrg  33391  ordtconnlem1  34101  outsideofeu  36344  matunitlindf  37866  ftc1anclem6  37946  cvrval5  39788  cdleme0ex2N  40597  dihglb2  41715  fimgmcyc  42901  mrefg2  43061  rmydioph  43368  islssfg2  43425  fsovrfovd  44362  elfz2z  47672