Theorem pm5.32d 588

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 584	. 2 ⊢ ((𝜓 → (𝜒 ↔ 𝜃)) ↔ ((𝜓 ∧ 𝜒) ↔ (𝜓 ∧ 𝜃)))
3	1, 2	sylib 221	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:  pm5.32rd  589  pm5.32da  590  anbi2d  642  raltpd  4745  opeqsng  5484  dfres3  5981  cores  6249  isoini  7343  eqfunresadj  7367  mpoeq123  7489  ordpwsuc  7815  xpord3pred  8154  rdglim2  8425  indpi1  12260  fzind  12723  btwnz  12728  elfzm11  13654  isprm2  16778  isprm3  16779  modprminv  16897  modprminveq  16898  isrngim2  20600  elimifd  33026  xrecex  33373  ordtconnlem1  34442  dfrdg4  36538  ee7.2aOLD  37088  expdioph  43872  cantnf2  44174  pm14.122b  45255  rexbidar  45277