Theorem sban 2427

Description: Conjunction inside and outside of a substitution are equivalent. (Contributed by NM, 14-May-1993.)

Assertion

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

Proof of Theorem sban

Step	Hyp	Ref	Expression
1		sbn 2419	. . 3 ⊢ ([𝑦 / 𝑥] ¬ (𝜑 → ¬ 𝜓) ↔ ¬ [𝑦 / 𝑥](𝜑 → ¬ 𝜓))
2		sbim 2423	. . . 4 ⊢ ([𝑦 / 𝑥](𝜑 → ¬ 𝜓) ↔ ([𝑦 / 𝑥]𝜑 → [𝑦 / 𝑥] ¬ 𝜓))
3		sbn 2419	. . . . 5 ⊢ ([𝑦 / 𝑥] ¬ 𝜓 ↔ ¬ [𝑦 / 𝑥]𝜓)
4	3	imbi2i 325	. . . 4 ⊢ (([𝑦 / 𝑥]𝜑 → [𝑦 / 𝑥] ¬ 𝜓) ↔ ([𝑦 / 𝑥]𝜑 → ¬ [𝑦 / 𝑥]𝜓))
5	2, 4	bitri 264	. . 3 ⊢ ([𝑦 / 𝑥](𝜑 → ¬ 𝜓) ↔ ([𝑦 / 𝑥]𝜑 → ¬ [𝑦 / 𝑥]𝜓))
6	1, 5	xchbinx 323	. 2 ⊢ ([𝑦 / 𝑥] ¬ (𝜑 → ¬ 𝜓) ↔ ¬ ([𝑦 / 𝑥]𝜑 → ¬ [𝑦 / 𝑥]𝜓))
7		df-an 385	. . 3 ⊢ ((𝜑 ∧ 𝜓) ↔ ¬ (𝜑 → ¬ 𝜓))
8	7	sbbii 1944	. 2 ⊢ ([𝑦 / 𝑥](𝜑 ∧ 𝜓) ↔ [𝑦 / 𝑥] ¬ (𝜑 → ¬ 𝜓))
9		df-an 385	. 2 ⊢ (([𝑦 / 𝑥]𝜑 ∧ [𝑦 / 𝑥]𝜓) ↔ ¬ ([𝑦 / 𝑥]𝜑 → ¬ [𝑦 / 𝑥]𝜓))
10	6, 8, 9	3bitr4i 292	1 ⊢ ([𝑦 / 𝑥](𝜑 ∧ 𝜓) ↔ ([𝑦 / 𝑥]𝜑 ∧ [𝑦 / 𝑥]𝜓))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 196   ∧ wa 383  [wsb 1937

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-10 2059  ax-12 2087  ax-13 2282

This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-ex 1745  df-nf 1750  df-sb 1938

This theorem is referenced by:  sb3an  2428  sbbi  2429  sbabel  2822  cbvreu  3199  sbcan  3511  rmo3  3561  inab  3928  difab  3929  exss  4961  inopab  5285  mo5f  29452  rmo3f  29462  iuninc  29505  suppss2f  29567  fmptdF  29584  disjdsct  29608  esumpfinvalf  30266  measiuns  30408  ballotlemodife  30687  sb5ALT  39048  sbcangOLD  39056  2uasbanh  39094  2uasbanhVD  39461  sb5ALTVD  39463  ellimcabssub0  40167