Theorem sban 2112

Description: Conjunction inside and outside of a substitution are equivalent. Compare 19.26 1889. (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 486	. . . 4 ⊢ ((𝜑 ∧ 𝜓) → 𝜑)
2	1	sbimi 2106	. . 3 ⊢ ([𝑦 / 𝑥](𝜑 ∧ 𝜓) → [𝑦 / 𝑥]𝜑)
3		simpr 488	. . . 4 ⊢ ((𝜑 ∧ 𝜓) → 𝜓)
4	3	sbimi 2106	. . 3 ⊢ ([𝑦 / 𝑥](𝜑 ∧ 𝜓) → [𝑦 / 𝑥]𝜓)
5	2, 4	jca 519	. 2 ⊢ ([𝑦 / 𝑥](𝜑 ∧ 𝜓) → ([𝑦 / 𝑥]𝜑 ∧ [𝑦 / 𝑥]𝜓))
6		pm3.2 473	. . . 4 ⊢ (𝜑 → (𝜓 → (𝜑 ∧ 𝜓)))
7	6	sb2imi 2107	. . 3 ⊢ ([𝑦 / 𝑥]𝜑 → ([𝑦 / 𝑥]𝜓 → [𝑦 / 𝑥](𝜑 ∧ 𝜓)))
8	7	imp 410	. 2 ⊢ (([𝑦 / 𝑥]𝜑 ∧ [𝑦 / 𝑥]𝜓) → [𝑦 / 𝑥](𝜑 ∧ 𝜓))
9	5, 8	impbii 211	1 ⊢ ([𝑦 / 𝑥](𝜑 ∧ 𝜓) ↔ ([𝑦 / 𝑥]𝜑 ∧ [𝑦 / 𝑥]𝜓))

Syntax hints:   ↔ wb 208   ∧ wa 399  [wsb 2089

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

This theorem depends on definitions:  df-bi 209  df-an 400  df-sb 2090

This theorem is referenced by:  sb3an  2113  sbbi  2340  sbabel  2955  cbvreu  3405  rmo3f  3696  sbcan  3793  rmo3  3842  inab  4261  difab  4262  exss  5429  inopab  5800  difopab  5801  mo5f  32636  iuninc  32709  suppss2f  32790  fmptdF  32808  disjdsct  32855  esumpfinvalf  34334  measiuns  34475  ballotlemodife  34756  xpab  36040  sbn1ALT  37307  sb5ALT  45065  2uasbanh  45101  2uasbanhVD  45450  sb5ALTVD  45452  ellimcabssub0  46157  ichan  48025