Metamath Proof Explorer

Theorem tradd

Description: Add top ad a conjunct. (Contributed by Giovanni Mascellani, 24-May-2019)

Ref Expression
Hypothesis tradd.1 
|- ( ph <-> ps )
Assertion tradd 
|- ( ph <-> ( T. /\ ps ) )

Proof

Step Hyp Ref Expression
1 tradd.1 
 |-  ( ph <-> ps )
2 truan 
 |-  ( ( T. /\ ps ) <-> ps )
3 1 2 bitr4i 
 |-  ( ph <-> ( T. /\ ps ) )