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 ⊢ (𝜑 → ((𝜓 ∧ 𝜒) ↔ (𝜓 ∧ 𝜃)))

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  455  pm5.32da  456  pm5.32  457  anbi2d  468  cbvex2  1978  cores  5289  isoini  6018  mpoeq123  6141  genpassl  7885  genpassu  7886  fzind  9744  btwnz  9748  elfzm11  10481  isprm2  12878  isprm3  12879  modprminv  13011  modprminveq  13012