Theorem triantru3

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

	Ref	Expression
Hypotheses	triantru3.1	⊢ 𝜑
	triantru3.2	⊢ 𝜓
Assertion	triantru3	⊢ ( 𝜒 ↔ ( 𝜑 ∧ 𝜓 ∧ 𝜒 ) )

Proof

Step	Hyp	Ref	Expression
1		triantru3.1	⊢ 𝜑
2		triantru3.2	⊢ 𝜓
3	1	biantrur	⊢ ( ( 𝜓 ∧ 𝜒 ) ↔ ( 𝜑 ∧ ( 𝜓 ∧ 𝜒 ) ) )
4	2	biantrur	⊢ ( 𝜒 ↔ ( 𝜓 ∧ 𝜒 ) )
5		3anass	⊢ ( ( 𝜑 ∧ 𝜓 ∧ 𝜒 ) ↔ ( 𝜑 ∧ ( 𝜓 ∧ 𝜒 ) ) )
6	3 4 5	3bitr4i	⊢ ( 𝜒 ↔ ( 𝜑 ∧ 𝜓 ∧ 𝜒 ) )