Theorem sban 2114

Description: Conjunction inside and outside of a substitution are equivalent. Compare 19.26 1900. (Contributed by NM, 14-May-1993.) (Proof shortened by Steven Nguyen, 13-Aug-2023.)

Assertion

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

Proof of Theorem sban

Step	Hyp	Ref	Expression
1		simpl 487	. . . 4 ⊢ ((𝜑 ∧ 𝜓) → 𝜑)
2	1	sbimi 2108	. . 3 ⊢ ([𝑦 / 𝑥](𝜑 ∧ 𝜓) → [𝑦 / 𝑥]𝜑)
3		simpr 489	. . . 4 ⊢ ((𝜑 ∧ 𝜓) → 𝜓)
4	3	sbimi 2108	. . 3 ⊢ ([𝑦 / 𝑥](𝜑 ∧ 𝜓) → [𝑦 / 𝑥]𝜓)
5	2, 4	jca 520	. 2 ⊢ ([𝑦 / 𝑥](𝜑 ∧ 𝜓) → ([𝑦 / 𝑥]𝜑 ∧ [𝑦 / 𝑥]𝜓))
6		pm3.2 474	. . . 4 ⊢ (𝜑 → (𝜓 → (𝜑 ∧ 𝜓)))
7	6	sb2imi 2109	. . 3 ⊢ ([𝑦 / 𝑥]𝜑 → ([𝑦 / 𝑥]𝜓 → [𝑦 / 𝑥](𝜑 ∧ 𝜓)))
8	7	imp 411	. 2 ⊢ (([𝑦 / 𝑥]𝜑 ∧ [𝑦 / 𝑥]𝜓) → [𝑦 / 𝑥](𝜑 ∧ 𝜓))
9	5, 8	impbii 212	1 ⊢ ([𝑦 / 𝑥](𝜑 ∧ 𝜓) ↔ ([𝑦 / 𝑥]𝜑 ∧ [𝑦 / 𝑥]𝜓))

Syntax hints:   ↔ wb 209   ∧ wa 400  [wsb 2096

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1810  df-sb 2097

This theorem is referenced by:  sb3an  2115  sbbi  2342  sbabel  2957  cbvreu  3408  rmo3f  3698  sbcan  3794  rmo3  3843  inab  4263  difab  4264  exss  5446  inopab  5818  difopab  5819  mo5f  32816  iuninc  32886  suppss2f  32964  fmptdF  32982  disjdsct  33029  esumpfinvalf  34447  measiuns  34588  ballotlemodife  34869  xpab  36199  sbn1ALT  37474  sb5ALT  45217  2uasbanh  45253  2uasbanhVD  45602  sb5ALTVD  45604  ellimcabssub0  46316  ichan  48187