Metamath Proof Explorer

Theorem anabs7

Description: Absorption into embedded conjunct. (Contributed by NM, 20-Jul-1996) (Proof shortened by Wolf Lammen, 17-Nov-2013)

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

Proof

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