Theorem pm5.32rd 670

Description: Distribution of implication over biconditional (deduction rule). (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 669	. 2 ⊢ (𝜑 → ((𝜓 ∧ 𝜒) ↔ (𝜓 ∧ 𝜃)))
3		ancom 465	. 2 ⊢ ((𝜒 ∧ 𝜓) ↔ (𝜓 ∧ 𝜒))
4		ancom 465	. 2 ⊢ ((𝜃 ∧ 𝜓) ↔ (𝜓 ∧ 𝜃))
5	2, 3, 4	3bitr4g 302	1 ⊢ (𝜑 → ((𝜒 ∧ 𝜓) ↔ (𝜃 ∧ 𝜓)))

Syntax hints:   → wi 4   ↔ wb 195   ∧ wa 383

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 196  df-an 385

This theorem is referenced by:  anbi1d  737  pm5.71  973  omord  7535  oeeui  7569  omxpenlem  7946  wemapwe  8477  fin23lem26  9030  1idpr  9730  repsdf2  13376  smueqlem  15050  tchcph  22844  isusgra0  25876  is2wlk  26095  wwlkn0s  26233  wwlkextwrd  26256  clwwlkn2  26303  2pthwlkonot  26412  rusgranumwlkl1  26474  rusgra0edg  26482  eupath2lem3  26506  ordtconlem1  29298  outsideofeu  31408  matunitlindf  32577  ftc1anclem6  32660  cvrval5  33719  cdleme0ex2N  34529  dihglb2  35649  mrefg2  36288  rmydioph  36599  islssfg2  36659  fsovrfovd  37323  elfz2z  40352  upgr2wlk  40876  upgrspths1wlk  40944  isspthonpth-av  40955  iswwlksnx  41042  wwlksnextwrd  41103  rusgrnumwwlkl1  41172  isclwwlksnx  41197  eupth2lem3lem6  41401