Theorem just3-df 2082

Description: Third justification theorem for definitions whose definiens is a conjunction, as in df-sb 2085. 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 2080, 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 531	. 2 ⊢ (𝜓 → (𝜓 ∧ (𝜓 ↔ 𝜒)))
3		just3-df.1	. . 3 ⊢ (𝜑 ↔ (𝜓 ∧ 𝜒))
4		abab 835	. . 3 ⊢ ((𝜓 ∧ 𝜒) ↔ (𝜓 ∧ (𝜓 ↔ 𝜒)))
5	3, 4	bitri 277	. 2 ⊢ (𝜑 ↔ (𝜓 ∧ (𝜓 ↔ 𝜒)))
6	2, 5	sylibr 236	1 ⊢ (𝜓 → 𝜑)

Syntax hints:   → wi 4   ↔ wb 208   ∧ wa 398

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 209  df-an 399

This theorem is referenced by:  dfsb  2087