Metamath Proof Explorer

Theorem bj-bisimpl

Description: Implication from equivalence with a conjunct. Its associated inference is simplbi . (Contributed by BJ, 20-Mar-2026)

Ref Expression
Assertion bj-bisimpl 
|- ( ( ph <-> ( ps /\ ch ) ) -> ( ph -> ps ) )

Proof

Step Hyp Ref Expression
1 biimp 
 |-  ( ( ph <-> ( ps /\ ch ) ) -> ( ph -> ( ps /\ ch ) ) )
2 simpl 
 |-  ( ( ps /\ ch ) -> ps )
3 1 2 syl6 
 |-  ( ( ph <-> ( ps /\ ch ) ) -> ( ph -> ps ) )