Theorem just3-df 2091

Description: Third justification theorem for definitions whose definiens is a conjunction, as in df-sb 2094. In addition to the defining equivalence, the second hypothesis requires the conjuncts of the definiens to be equivalent.

When the conjuncts are quantified and differ only by a bound-variable renaming, this equivalence is usually obtained from an implicit substitution between the underlying expressions. In some cases, however, it can be proved more directly and with fewer axioms.

Under these assumptions, either conjunct implies the definiendum. Together with just1-df 2089, the definiendum is therefore equivalent to either conjunct. (Contributed by Wolf Lammen, 6-Jun-2026.)

Hypotheses

Ref	Expression
just3-df.1	⊢ (𝜑 ↔ (𝜓 ∧ 𝜒))
just3-df.2	⊢ (𝜓 ↔ 𝜒)

Assertion

Ref	Expression
just3-df	⊢ (𝜓 → 𝜑)

Proof of Theorem just3-df

Step	Hyp	Ref	Expression
1		just3-df.2	. . 3 ⊢ (𝜓 ↔ 𝜒)
2	1	jctr 533	. 2 ⊢ (𝜓 → (𝜓 ∧ (𝜓 ↔ 𝜒)))
3		just3-df.1	. . 3 ⊢ (𝜑 ↔ (𝜓 ∧ 𝜒))
4		abab 839	. . 3 ⊢ ((𝜓 ∧ 𝜒) ↔ (𝜓 ∧ (𝜓 ↔ 𝜒)))
5	3, 4	bitri 278	. 2 ⊢ (𝜑 ↔ (𝜓 ∧ (𝜓 ↔ 𝜒)))
6	2, 5	sylibr 237	1 ⊢ (𝜓 → 𝜑)

Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 400

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 210  df-an 401

This theorem is referenced by:  dfsb  2096