Theorem pm5.32rd 570

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

Syntax hints:   → wi 4   ↔ wb 198   ∧ wa 387

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 199  df-an 388

This theorem is referenced by:  anbi1d  620  pm5.71  1010  omord  7997  oeeui  8031  omxpenlem  8416  wemapwe  8956  fin23lem26  9547  1idpr  10251  repsdf2  14000  smueqlem  15702  tcphcph  23546  2sqreultlem  25728  2sqreunnltlem  25731  upgr2wlk  27155  upgrspthswlk  27230  isspthonpth  27241  iswwlksnx  27329  wwlksnextwrd  27391  wwlksnextwrdOLD  27396  rusgrnumwwlkl1  27477  isclwwlknx  27554  clwwlknwwlksnb  27581  clwwlknonel  27626  eupth2lem3lem6  27766  ordtconnlem1  30811  outsideofeu  33113  matunitlindf  34331  ftc1anclem6  34413  cvrval5  35996  cdleme0ex2N  36805  dihglb2  37923  mrefg2  38699  rmydioph  39007  islssfg2  39067  fsovrfovd  39718  elfz2z  42922