Theorem pm5.32rd 586

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

Syntax hints:   → wi 4   ↔ wb 208   ∧ wa 399

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 209  df-an 400

This theorem is referenced by:  anbi1d  640  pm5.71  1040  omord  8531  oeeui  8566  omxpenlem  9044  wemapwe  9646  fin23lem26  10276  1idpr  10981  repsdf2  14785  smueqlem  16515  tcphcph  25287  2sqreultlem  27499  2sqreunnltlem  27502  n0cutlt  28440  upgr2wlk  29824  upgrspthswlk  29895  isspthonpth  29906  iswwlksnx  29997  wwlksnextwrd  30054  rusgrnumwwlkl1  30128  isclwwlknx  30195  clwwlknwwlksnb  30214  clwwlknonel  30254  eupth2lem3lem6  30392  subsdrg  33446  ordtconnlem1  34182  outsideofeu  36442  matunitlindf  38078  ftc1anclem6  38158  cvrval5  40000  cdleme0ex2N  40809  dihglb2  41927  fimgmcyc  43113  mrefg2  43249  rmydioph  43552  islssfg2  43609  fsovrfovd  44546  elfz2z  47870