Theorem sban 1984

Description: Conjunction inside and outside of a substitution are equivalent. (Contributed by NM, 5-Aug-1993.) (Proof rewritten by Jim Kingdon, 3-Feb-2018.)

Assertion

Ref	Expression
sban	⊢ ([𝑦 / 𝑥](𝜑 ∧ 𝜓) ↔ ([𝑦 / 𝑥]𝜑 ∧ [𝑦 / 𝑥]𝜓))

Proof of Theorem sban

Dummy variable 𝑧 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		sbanv 1914	. . . 4 ⊢ ([𝑧 / 𝑥](𝜑 ∧ 𝜓) ↔ ([𝑧 / 𝑥]𝜑 ∧ [𝑧 / 𝑥]𝜓))
2	1	sbbii 1789	. . 3 ⊢ ([𝑦 / 𝑧][𝑧 / 𝑥](𝜑 ∧ 𝜓) ↔ [𝑦 / 𝑧]([𝑧 / 𝑥]𝜑 ∧ [𝑧 / 𝑥]𝜓))
3		sbanv 1914	. . 3 ⊢ ([𝑦 / 𝑧]([𝑧 / 𝑥]𝜑 ∧ [𝑧 / 𝑥]𝜓) ↔ ([𝑦 / 𝑧][𝑧 / 𝑥]𝜑 ∧ [𝑦 / 𝑧][𝑧 / 𝑥]𝜓))
4	2, 3	bitri 184	. 2 ⊢ ([𝑦 / 𝑧][𝑧 / 𝑥](𝜑 ∧ 𝜓) ↔ ([𝑦 / 𝑧][𝑧 / 𝑥]𝜑 ∧ [𝑦 / 𝑧][𝑧 / 𝑥]𝜓))
5		ax-17 1550	. . 3 ⊢ ((𝜑 ∧ 𝜓) → ∀𝑧(𝜑 ∧ 𝜓))
6	5	sbco2vh 1974	. 2 ⊢ ([𝑦 / 𝑧][𝑧 / 𝑥](𝜑 ∧ 𝜓) ↔ [𝑦 / 𝑥](𝜑 ∧ 𝜓))
7		ax-17 1550	. . . 4 ⊢ (𝜑 → ∀𝑧𝜑)
8	7	sbco2vh 1974	. . 3 ⊢ ([𝑦 / 𝑧][𝑧 / 𝑥]𝜑 ↔ [𝑦 / 𝑥]𝜑)
9		ax-17 1550	. . . 4 ⊢ (𝜓 → ∀𝑧𝜓)
10	9	sbco2vh 1974	. . 3 ⊢ ([𝑦 / 𝑧][𝑧 / 𝑥]𝜓 ↔ [𝑦 / 𝑥]𝜓)
11	8, 10	anbi12i 460	. 2 ⊢ (([𝑦 / 𝑧][𝑧 / 𝑥]𝜑 ∧ [𝑦 / 𝑧][𝑧 / 𝑥]𝜓) ↔ ([𝑦 / 𝑥]𝜑 ∧ [𝑦 / 𝑥]𝜓))
12	4, 6, 11	3bitr3i 210	1 ⊢ ([𝑦 / 𝑥](𝜑 ∧ 𝜓) ↔ ([𝑦 / 𝑥]𝜑 ∧ [𝑦 / 𝑥]𝜓))

Syntax hints:   ∧ wa 104   ↔ wb 105  [wsb 1786

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 711  ax-5 1471  ax-7 1472  ax-gen 1473  ax-ie1 1517  ax-ie2 1518  ax-8 1528  ax-10 1529  ax-11 1530  ax-i12 1531  ax-4 1534  ax-17 1550  ax-i9 1554  ax-ial 1558  ax-i5r 1559

This theorem depends on definitions:  df-bi 117  df-nf 1485  df-sb 1787

This theorem is referenced by:  sb3an  1987  sbbi  1988  sbmo  2114  moanim  2129  sbabel  2376  nfrexdya  2543  cbvreu  2737  rmo3f  2971  sbcan  3042  sbcang  3043  rmo3  3091  inab  3442  difab  3443  exss  4275  inopab  4814  bdcriota  15893