Theorem pm5.32rd 589

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  anbi1d  643  pm5.71  1045  omord  8614  oeeui  8649  omxpenlem  9135  wemapwe  9735  fin23lem26  10442  1idpr  11153  repsdf2  14971  smueqlem  16704  matunitlindf  23051  tcphcph  25613  2sqreultlem  27831  2sqreunnltlem  27834  n0cutlt  28802  upgr2wlk  30304  upgrspthswlk  30381  isspthonpth  30392  iswwlksnx  30486  wwlksnextwrd  30543  rusgrnumwwlkl1  30617  isclwwlknx  30684  clwwlknwwlksnb  30703  clwwlknonel  30743  eupth2lem3lem6  30891  subsdrg  33964  ordtconnlem1  34667  outsideofeu  37111  ftc1anclem6  38884  cvrval5  40738  cdleme0ex2N  41547  dihglb2  42665  fimgmcyc  43864  mrefg2  43984  rmydioph  44287  islssfg2  44339  fsovrfovd  45270  elfz2z  48658