This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.
Database CLASSICAL FIRST-ORDER LOGIC WITH EQUALITY Predicate calculus with equality: Tarski's system S2 (1 rule, 6 schemes) Define proper substitution sban
Description: Conjunction inside and outside of a substitution are equivalent. Compare
19.26 . (Contributed by NM , 14-May-1993) (Proof shortened by Steven
Nguyen , 13-Aug-2023)
Ref
Expression
Assertion
sban ⊢ y x φ ∧ ψ ↔ y x φ ∧ y x ψ
Proof
Step
Hyp
Ref
Expression
1
simpl ⊢ φ ∧ ψ → φ
2
1
sbimi ⊢ y x φ ∧ ψ → y x φ
3
simpr ⊢ φ ∧ ψ → ψ
4
3
sbimi ⊢ y x φ ∧ ψ → y x ψ
5
2 4
jca ⊢ y x φ ∧ ψ → y x φ ∧ y x ψ
6
pm3.2 ⊢ φ → ψ → φ ∧ ψ
7
6
sb2imi ⊢ y x φ → y x ψ → y x φ ∧ ψ
8
7
imp ⊢ y x φ ∧ y x ψ → y x φ ∧ ψ
9
5 8
impbii ⊢ y x φ ∧ ψ ↔ y x φ ∧ y x ψ