Metamath Proof Explorer

Theorem pm4.38

Description: Theorem *4.38 of WhiteheadRussell p. 118. (Contributed by NM, 3-Jan-2005)

		Ref	Expression
	Assertion	pm4.38	$⊢ ((φ \leftrightarrow χ) \land (ψ \leftrightarrow θ)) \to ((φ \land ψ) \leftrightarrow (χ \land θ))$

Step	Hyp	Ref	Expression
1		simpl	$⊢ ((φ \leftrightarrow χ) \land (ψ \leftrightarrow θ)) \to (φ \leftrightarrow χ)$
2		simpr	$⊢ ((φ \leftrightarrow χ) \land (ψ \leftrightarrow θ)) \to (ψ \leftrightarrow θ)$
3	1 2	anbi12d	$⊢ ((φ \leftrightarrow χ) \land (ψ \leftrightarrow θ)) \to ((φ \land ψ) \leftrightarrow (χ \land θ))$