Theorem pm5.32d 450

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 447	. 2 ⊢ (𝜑 → ((𝜓 ∧ 𝜒) → (𝜓 ∧ 𝜃)))
5		biimpr 130	. . . 4 ⊢ ((𝜒 ↔ 𝜃) → (𝜃 → 𝜒))
6	1, 5	syl6 33	. . 3 ⊢ (𝜑 → (𝜓 → (𝜃 → 𝜒)))
7	6	imdistand 447	. 2 ⊢ (𝜑 → ((𝜓 ∧ 𝜃) → (𝜓 ∧ 𝜒)))
8	4, 7	impbid 129	1 ⊢ (𝜑 → ((𝜓 ∧ 𝜒) ↔ (𝜓 ∧ 𝜃)))

Syntax hints:   → wi 4   ∧ wa 104   ↔ wb 105

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  pm5.32rd  451  pm5.32da  452  pm5.32  453  anbi2d  464  cbvex2  1947  cores  5206  isoini  5912  mpoeq123  6029  genpassl  7674  genpassu  7675  fzind  9525  btwnz  9529  elfzm11  10250  isprm2  12600  isprm3  12601  modprminv  12733  modprminveq  12734