Metamath Proof Explorer

Theorem truconj

Description: Add true as a conjunct. (Contributed by Giovanni Mascellani, 23-May-2019)

Ref Expression
Assertion truconj 
|- ( ph <-> ( T. /\ ph ) )

Proof

Step Hyp Ref Expression
1 truan 
 |-  ( ( T. /\ ph ) <-> ph )
2 1 bicomi 
 |-  ( ph <-> ( T. /\ ph ) )