Metamath Proof Explorer

Theorem anabs1

Description: Absorption into embedded conjunct. (Contributed by NM, 4-Sep-1995) (Proof shortened by Wolf Lammen, 16-Nov-2013)

Ref Expression
Assertion anabs1 
|- ( ( ( ph /\ ps ) /\ ph ) <-> ( ph /\ ps ) )

Proof

Step Hyp Ref Expression
1 simpl 
 |-  ( ( ph /\ ps ) -> ph )
2 1 pm4.71i 
 |-  ( ( ph /\ ps ) <-> ( ( ph /\ ps ) /\ ph ) )
3 2 bicomi 
 |-  ( ( ( ph /\ ps ) /\ ph ) <-> ( ph /\ ps ) )