Theorem just3-df

Description: Third justification theorem for definitions whose definiens is a conjunction, as in df-sb . 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 , the definiendum is therefore equivalent to either conjunct. (Contributed by Wolf Lammen, 6-Jun-2026)

	Ref	Expression
Hypotheses	just3-df.1	|- ( ph <-> ( ps /\ ch ) )
	just3-df.2	|- ( ps <-> ch )
Assertion	just3-df	|- ( ps -> ph )

Proof

Step	Hyp	Ref	Expression
1		just3-df.1	|- ( ph <-> ( ps /\ ch ) )
2		just3-df.2	|- ( ps <-> ch )
3	2	jctr	|- ( ps -> ( ps /\ ( ps <-> ch ) ) )
4		abab	|- ( ( ps /\ ch ) <-> ( ps /\ ( ps <-> ch ) ) )
5	1 4	bitri	|- ( ph <-> ( ps /\ ( ps <-> ch ) ) )
6	3 5	sylibr	|- ( ps -> ph )