Theorem pm5.32rd 583

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 582	. 2 ⊢ (𝜑 → ((𝜓 ∧ 𝜒) ↔ (𝜓 ∧ 𝜃)))
3		ancom 461	. 2 ⊢ ((𝜒 ∧ 𝜓) ↔ (𝜓 ∧ 𝜒))
4		ancom 461	. 2 ⊢ ((𝜃 ∧ 𝜓) ↔ (𝜓 ∧ 𝜃))
5	2, 3, 4	3bitr4g 315	1 ⊢ (𝜑 → ((𝜒 ∧ 𝜓) ↔ (𝜃 ∧ 𝜓)))

Syntax hints:   → wi 4   ↔ wb 207   ∧ wa 396

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 208  df-an 397

This theorem is referenced by:  anbi1d  637  pm5.71  1035  omord  8493  oeeui  8528  omxpenlem  9006  wemapwe  9609  fin23lem26  10238  1idpr  10943  repsdf2  14731  smueqlem  16450  tcphcph  25222  2sqreultlem  27428  2sqreunnltlem  27431  n0cutlt  28369  upgr2wlk  29753  upgrspthswlk  29824  isspthonpth  29835  iswwlksnx  29926  wwlksnextwrd  29983  rusgrnumwwlkl1  30057  isclwwlknx  30124  clwwlknwwlksnb  30143  clwwlknonel  30183  eupth2lem3lem6  30321  subsdrg  33382  ordtconnlem1  34108  outsideofeu  36359  matunitlindf  37985  ftc1anclem6  38065  cvrval5  39907  cdleme0ex2N  40716  dihglb2  41834  fimgmcyc  43020  mrefg2  43156  rmydioph  43459  islssfg2  43516  fsovrfovd  44453  elfz2z  47778