Metamath Proof Explorer

Theorem sbor2

Description: One direction of sbor , using fewer axioms. Compare 19.33 . (Contributed by Steven Nguyen, 18-Aug-2023)

Ref Expression
Assertion sbor2 
|- ( ( [ t / x ] ph \/ [ t / x ] ps ) -> [ t / x ] ( ph \/ ps ) )

Proof

Step Hyp Ref Expression
1 orc 
 |-  ( ph -> ( ph \/ ps ) )
2 1 sbimi 
 |-  ( [ t / x ] ph -> [ t / x ] ( ph \/ ps ) )
3 olc 
 |-  ( ps -> ( ph \/ ps ) )
4 3 sbimi 
 |-  ( [ t / x ] ps -> [ t / x ] ( ph \/ ps ) )
5 2 4 jaoi 
 |-  ( ( [ t / x ] ph \/ [ t / x ] ps ) -> [ t / x ] ( ph \/ ps ) )