This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem mpbiran3d

Description: Equivalence with a conjunction one of whose conjuncts is a consequence of the other. Deduction form. (Contributed by Zhi Wang, 24-Sep-2024)

	Ref	Expression
Hypotheses	mpbiran3d.1	$⊢ φ \to (ψ \leftrightarrow (χ \land θ))$
	mpbiran3d.2	$⊢ (φ \land χ) \to θ$
Assertion	mpbiran3d	$⊢ φ \to (ψ \leftrightarrow χ)$

Proof

Step	Hyp	Ref	Expression
1		mpbiran3d.1	$⊢ φ \to (ψ \leftrightarrow (χ \land θ))$
2		mpbiran3d.2	$⊢ (φ \land χ) \to θ$
3	1	simprbda	$⊢ (φ \land ψ) \to χ$
4	3	ex	$⊢ φ \to (ψ \to χ)$
5	2	ex	$⊢ φ \to (χ \to θ)$
6	5	ancld	$⊢ φ \to (χ \to (χ \land θ))$
7	6 1	sylibrd	$⊢ φ \to (χ \to ψ)$
8	4 7	impbid	$⊢ φ \to (ψ \leftrightarrow χ)$