Theorem pm5.32d 577

Description: Distribution of implication over biconditional (deduction form). (Contributed by NM, 29-Oct-1996.)

Hypothesis

Ref	Expression
pm5.32d.1	⊢ (𝜑 → (𝜓 → (𝜒 ↔ 𝜃)))

Assertion

Ref	Expression
pm5.32d	⊢ (𝜑 → ((𝜓 ∧ 𝜒) ↔ (𝜓 ∧ 𝜃)))

Proof of Theorem pm5.32d

Step	Hyp	Ref	Expression
1		pm5.32d.1	. 2 ⊢ (𝜑 → (𝜓 → (𝜒 ↔ 𝜃)))
2		pm5.32 573	. 2 ⊢ ((𝜓 → (𝜒 ↔ 𝜃)) ↔ ((𝜓 ∧ 𝜒) ↔ (𝜓 ∧ 𝜃)))
3	1, 2	sylib 218	1 ⊢ (𝜑 → ((𝜓 ∧ 𝜒) ↔ (𝜓 ∧ 𝜃)))

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395

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 207  df-an 396

This theorem is referenced by:  pm5.32rd  578  pm5.32da  579  anbi2d  630  raltpd  4734  opeqsng  5443  dfres3  5933  cores  6196  isoini  7272  eqfunresadj  7294  mpoeq123  7418  ordpwsuc  7745  xpord3pred  8082  rdglim2  8351  fzind  12568  btwnz  12573  elfzm11  13492  isprm2  16590  isprm3  16591  modprminv  16708  modprminveq  16709  isrngim2  20369  bian1d  32430  elimifd  32518  indpi1  32836  xrecex  32895  ordtconnlem1  33932  dfrdg4  35984  ee7.2aOLD  36494  wl-ax11-lem8  37625  expdioph  43055  cantnf2  43357  pm14.122b  44455  rexbidar  44477