Theorem pm5.32d 454

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

Hypothesis

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

Assertion

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

Proof of Theorem pm5.32d

Step	Hyp	Ref	Expression
1		pm5.32d.1	. . . 4 ⊢ (𝜑 → (𝜓 → (𝜒 ↔ 𝜃)))
2		biimp 118	. . . 4 ⊢ ((𝜒 ↔ 𝜃) → (𝜒 → 𝜃))
3	1, 2	syl6 33	. . 3 ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃)))
4	3	imdistand 451	. 2 ⊢ (𝜑 → ((𝜓 ∧ 𝜒) → (𝜓 ∧ 𝜃)))
5		biimpr 130	. . . 4 ⊢ ((𝜒 ↔ 𝜃) → (𝜃 → 𝜒))
6	1, 5	syl6 33	. . 3 ⊢ (𝜑 → (𝜓 → (𝜃 → 𝜒)))
7	6	imdistand 451	. 2 ⊢ (𝜑 → ((𝜓 ∧ 𝜃) → (𝜓 ∧ 𝜒)))
8	4, 7	impbid 129	1 ⊢ (𝜑 → ((𝜓 ∧ 𝜒) ↔ (𝜓 ∧ 𝜃)))

This proof depends on syntax axioms:   → wi 4   ∧ wa 104   ↔ wb 105

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This proof depends on definitions:  df-bi 117

This theorem is used by:  pm5.32rd  455  pm5.32da  456  pm5.32  457  anbi2d  468  cbvex2  1978  cores  5294  isoini  6027  mpoeq123  6150  genpassl  7898  genpassu  7899  fzind  9773  btwnz  9777  elfzm11  10516  isprm2  12921  isprm3  12922  modprminv  13058  modprminveq  13059