Metamath Proof Explorer


Theorem sbcbi

Description: Implication form of sbcbii . sbcbi is sbcbiVD without virtual deductions and was automatically derived from sbcbiVD using the tools program translate..without..overwriting.cmd and Metamath's minimize command. (Contributed by Alan Sare, 18-Mar-2012) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Assertion sbcbi ( 𝐴𝑉 → ( ∀ 𝑥 ( 𝜑𝜓 ) → ( [ 𝐴 / 𝑥 ] 𝜑[ 𝐴 / 𝑥 ] 𝜓 ) ) )

Proof

Step Hyp Ref Expression
1 spsbc ( 𝐴𝑉 → ( ∀ 𝑥 ( 𝜑𝜓 ) → [ 𝐴 / 𝑥 ] ( 𝜑𝜓 ) ) )
2 sbcbig ( 𝐴𝑉 → ( [ 𝐴 / 𝑥 ] ( 𝜑𝜓 ) ↔ ( [ 𝐴 / 𝑥 ] 𝜑[ 𝐴 / 𝑥 ] 𝜓 ) ) )
3 1 2 sylibd ( 𝐴𝑉 → ( ∀ 𝑥 ( 𝜑𝜓 ) → ( [ 𝐴 / 𝑥 ] 𝜑[ 𝐴 / 𝑥 ] 𝜓 ) ) )