Theorem triantru3

Description: A wff is equivalent to its conjunctions with truths. (Contributed by Peter Mazsa, 30-Nov-2018)

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

Proof

Step	Hyp	Ref	Expression
1		triantru3.1	|- ph
2		triantru3.2	|- ps
3	1	biantrur	|- ( ( ps /\ ch ) <-> ( ph /\ ( ps /\ ch ) ) )
4	2	biantrur	|- ( ch <-> ( ps /\ ch ) )
5		3anass	|- ( ( ph /\ ps /\ ch ) <-> ( ph /\ ( ps /\ ch ) ) )
6	3 4 5	3bitr4i	|- ( ch <-> ( ph /\ ps /\ ch ) )