This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ⊢ ( 𝜒 ↔ ( 𝜑 ∧ 𝜓 ∧ 𝜒 ) )