Theorem sban 2117

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

This proof depends on syntax axioms:   ↔ wb 209   ∧ wa 401  [wsb 2099

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-sb 2100

This theorem is used by:  sb3an  2118  sbbi  2341  sbabel  2955  cbvreu  3405  rmo3f  3692  sbcan  3788  rmo3  3836  inab  4255  difab  4256  exss  5431  inopab  5807  difopab  5808  mo5f  33067  iuninc  33137  suppss2f  33214  fmptdf2  33232  disjdsct  33278  esumpfinvalf  34690  measiuns  34832  ballotlemodife  35113  xpab  36460  sbn1ALT  37740  sb5ALT  45467  2uasbanh  45503  2uasbanhVD  45852  sb5ALTVD  45854  ellimcabssub0  46573  ichan  48481