Theorem sban 2116

Description: Conjunction inside and outside of a substitution are equivalent. Compare 19.26 1893. (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 2110	. . 3 ⊢ ([𝑦 / 𝑥](𝜑 ∧ 𝜓) → [𝑦 / 𝑥]𝜑)
3		simpr 489	. . . 4 ⊢ ((𝜑 ∧ 𝜓) → 𝜓)
4	3	sbimi 2110	. . 3 ⊢ ([𝑦 / 𝑥](𝜑 ∧ 𝜓) → [𝑦 / 𝑥]𝜓)
5	2, 4	jca 520	. 2 ⊢ ([𝑦 / 𝑥](𝜑 ∧ 𝜓) → ([𝑦 / 𝑥]𝜑 ∧ [𝑦 / 𝑥]𝜓))
6		pm3.2 474	. . . 4 ⊢ (𝜑 → (𝜓 → (𝜑 ∧ 𝜓)))
7	6	sb2imi 2111	. . 3 ⊢ ([𝑦 / 𝑥]𝜑 → ([𝑦 / 𝑥]𝜓 → [𝑦 / 𝑥](𝜑 ∧ 𝜓)))
8	7	imp 411	. 2 ⊢ (([𝑦 / 𝑥]𝜑 ∧ [𝑦 / 𝑥]𝜓) → [𝑦 / 𝑥](𝜑 ∧ 𝜓))
9	5, 8	impbii 212	1 ⊢ ([𝑦 / 𝑥](𝜑 ∧ 𝜓) ↔ ([𝑦 / 𝑥]𝜑 ∧ [𝑦 / 𝑥]𝜓))

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832

This theorem depends on definitions:  df-bi 210  df-an 401  df-sb 2094

This theorem is referenced by:  sb3an  2117  sbbi  2344  sbabel  2959  cbvreu  3409  rmo3f  3700  sbcan  3796  rmo3  3845  inab  4264  difab  4265  exss  5434  inopab  5806  difopab  5807  mo5f  32741  iuninc  32811  suppss2f  32891  fmptdF  32909  disjdsct  32956  esumpfinvalf  34378  measiuns  34519  ballotlemodife  34800  xpab  36084  sbn1ALT  37350  sb5ALT  45093  2uasbanh  45129  2uasbanhVD  45478  sb5ALTVD  45480  ellimcabssub0  46192  ichan  48060