Theorem sban 2083

Description: Conjunction inside and outside of a substitution are equivalent. Compare 19.26 1871. (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 482	. . . 4 ⊢ ((𝜑 ∧ 𝜓) → 𝜑)
2	1	sbimi 2077	. . 3 ⊢ ([𝑦 / 𝑥](𝜑 ∧ 𝜓) → [𝑦 / 𝑥]𝜑)
3		simpr 484	. . . 4 ⊢ ((𝜑 ∧ 𝜓) → 𝜓)
4	3	sbimi 2077	. . 3 ⊢ ([𝑦 / 𝑥](𝜑 ∧ 𝜓) → [𝑦 / 𝑥]𝜓)
5	2, 4	jca 511	. 2 ⊢ ([𝑦 / 𝑥](𝜑 ∧ 𝜓) → ([𝑦 / 𝑥]𝜑 ∧ [𝑦 / 𝑥]𝜓))
6		pm3.2 469	. . . 4 ⊢ (𝜑 → (𝜓 → (𝜑 ∧ 𝜓)))
7	6	sb2imi 2078	. . 3 ⊢ ([𝑦 / 𝑥]𝜑 → ([𝑦 / 𝑥]𝜓 → [𝑦 / 𝑥](𝜑 ∧ 𝜓)))
8	7	imp 406	. 2 ⊢ (([𝑦 / 𝑥]𝜑 ∧ [𝑦 / 𝑥]𝜓) → [𝑦 / 𝑥](𝜑 ∧ 𝜓))
9	5, 8	impbii 209	1 ⊢ ([𝑦 / 𝑥](𝜑 ∧ 𝜓) ↔ ([𝑦 / 𝑥]𝜑 ∧ [𝑦 / 𝑥]𝜓))

Syntax hints:   ↔ wb 206   ∧ wa 395  [wsb 2067

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

This theorem depends on definitions:  df-bi 207  df-an 396  df-sb 2068

This theorem is referenced by:  sb3an  2084  sbbi  2309  sbabel  2927  cbvreu  3387  rmo3f  3693  sbcan  3791  rmo3  3840  inab  4259  difab  4260  exss  5403  inopab  5769  difopab  5770  mo5f  32463  iuninc  32535  suppss2f  32615  fmptdF  32633  disjdsct  32679  esumpfinvalf  34084  measiuns  34225  ballotlemodife  34506  xpab  35758  sbn1ALT  36891  sb5ALT  44557  2uasbanh  44593  2uasbanhVD  44942  sb5ALTVD  44944  ellimcabssub0  45656  ichan  47485