ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  sban Unicode version

Theorem sban 1872
Description: Conjunction inside and outside of a substitution are equivalent. (Contributed by NM, 5-Aug-1993.) (Proof rewritten by Jim Kingdon, 3-Feb-2018.)
Assertion
Ref Expression
sban  |-  ( [ y  /  x ]
( ph  /\  ps )  <->  ( [ y  /  x ] ph  /\  [ y  /  x ] ps ) )

Proof of Theorem sban
Dummy variable  z is distinct from all other variables.
StepHypRef Expression
1 sbanv 1812 . . . 4  |-  ( [ z  /  x ]
( ph  /\  ps )  <->  ( [ z  /  x ] ph  /\  [ z  /  x ] ps ) )
21sbbii 1690 . . 3  |-  ( [ y  /  z ] [ z  /  x ] ( ph  /\  ps )  <->  [ y  /  z ] ( [ z  /  x ] ph  /\ 
[ z  /  x ] ps ) )
3 sbanv 1812 . . 3  |-  ( [ y  /  z ] ( [ z  /  x ] ph  /\  [
z  /  x ] ps )  <->  ( [ y  /  z ] [
z  /  x ] ph  /\  [ y  / 
z ] [ z  /  x ] ps ) )
42, 3bitri 182 . 2  |-  ( [ y  /  z ] [ z  /  x ] ( ph  /\  ps )  <->  ( [ y  /  z ] [
z  /  x ] ph  /\  [ y  / 
z ] [ z  /  x ] ps ) )
5 ax-17 1460 . . 3  |-  ( (
ph  /\  ps )  ->  A. z ( ph  /\ 
ps ) )
65sbco2v 1864 . 2  |-  ( [ y  /  z ] [ z  /  x ] ( ph  /\  ps )  <->  [ y  /  x ] ( ph  /\  ps ) )
7 ax-17 1460 . . . 4  |-  ( ph  ->  A. z ph )
87sbco2v 1864 . . 3  |-  ( [ y  /  z ] [ z  /  x ] ph  <->  [ y  /  x ] ph )
9 ax-17 1460 . . . 4  |-  ( ps 
->  A. z ps )
109sbco2v 1864 . . 3  |-  ( [ y  /  z ] [ z  /  x ] ps  <->  [ y  /  x ] ps )
118, 10anbi12i 448 . 2  |-  ( ( [ y  /  z ] [ z  /  x ] ph  /\  [ y  /  z ] [
z  /  x ] ps )  <->  ( [ y  /  x ] ph  /\ 
[ y  /  x ] ps ) )
124, 6, 113bitr3i 208 1  |-  ( [ y  /  x ]
( ph  /\  ps )  <->  ( [ y  /  x ] ph  /\  [ y  /  x ] ps ) )
Colors of variables: wff set class
Syntax hints:    /\ wa 102    <-> wb 103   [wsb 1687
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-io 663  ax-5 1377  ax-7 1378  ax-gen 1379  ax-ie1 1423  ax-ie2 1424  ax-8 1436  ax-10 1437  ax-11 1438  ax-i12 1439  ax-4 1441  ax-17 1460  ax-i9 1464  ax-ial 1468  ax-i5r 1469
This theorem depends on definitions:  df-bi 115  df-nf 1391  df-sb 1688
This theorem is referenced by:  sb3an  1875  sbbi  1876  sbmo  2002  moanim  2017  sbabel  2248  nfrexdya  2406  cbvreu  2580  sbcan  2865  sbcang  2866  rmo3  2914  inab  3248  difab  3249  exss  4010  inopab  4516  bdcriota  10959
  Copyright terms: Public domain W3C validator