Metamath Proof Explorer


Theorem sbcori

Description: Distribution of class substitution over disjunction, in inference form. (Contributed by Giovanni Mascellani, 27-May-2019)

Ref Expression
Hypotheses sbcori.1 ( [ 𝐴 / 𝑥 ] 𝜑𝜒 )
sbcori.2 ( [ 𝐴 / 𝑥 ] 𝜓𝜂 )
Assertion sbcori ( [ 𝐴 / 𝑥 ] ( 𝜑𝜓 ) ↔ ( 𝜒𝜂 ) )

Proof

Step Hyp Ref Expression
1 sbcori.1 ( [ 𝐴 / 𝑥 ] 𝜑𝜒 )
2 sbcori.2 ( [ 𝐴 / 𝑥 ] 𝜓𝜂 )
3 sbcor ( [ 𝐴 / 𝑥 ] ( 𝜑𝜓 ) ↔ ( [ 𝐴 / 𝑥 ] 𝜑[ 𝐴 / 𝑥 ] 𝜓 ) )
4 1 2 orbi12i ( ( [ 𝐴 / 𝑥 ] 𝜑[ 𝐴 / 𝑥 ] 𝜓 ) ↔ ( 𝜒𝜂 ) )
5 3 4 bitri ( [ 𝐴 / 𝑥 ] ( 𝜑𝜓 ) ↔ ( 𝜒𝜂 ) )