Metamath Proof Explorer

Theorem oranabs

Description: Absorb a disjunct into a conjunct. (Contributed by Roy F. Longton, 23-Jun-2005) (Proof shortened by Wolf Lammen, 10-Nov-2013)

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

Proof

Step Hyp Ref Expression
1 biortn 
 |-  ( ps -> ( ph <-> ( -. ps \/ ph ) ) )
2 orcom 
 |-  ( ( -. ps \/ ph ) <-> ( ph \/ -. ps ) )
3 1 2 bitr2di 
 |-  ( ps -> ( ( ph \/ -. ps ) <-> ph ) )
4 3 pm5.32ri 
 |-  ( ( ( ph \/ -. ps ) /\ ps ) <-> ( ph /\ ps ) )