Metamath Proof Explorer

Theorem 3anidm

Description: Idempotent law for conjunction. (Contributed by Peter Mazsa, 17-Oct-2023)

Ref Expression
Assertion 3anidm 
|- ( ( ph /\ ph /\ ph ) <-> ph )

Proof

Step Hyp Ref Expression
1 df-3an 
 |-  ( ( ph /\ ph /\ ph ) <-> ( ( ph /\ ph ) /\ ph ) )
2 anabs1 
 |-  ( ( ( ph /\ ph ) /\ ph ) <-> ( ph /\ ph ) )
3 anidm 
 |-  ( ( ph /\ ph ) <-> ph )
4 1 2 3 3bitri 
 |-  ( ( ph /\ ph /\ ph ) <-> ph )