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

Theorem sban 1874
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 1814 . . . 4  |-  ( [ z  /  x ]
( ph  /\  ps )  <->  ( [ z  /  x ] ph  /\  [ z  /  x ] ps ) )
21sbbii 1692 . . 3  |-  ( [ y  /  z ] [ z  /  x ] ( ph  /\  ps )  <->  [ y  /  z ] ( [ z  /  x ] ph  /\ 
[ z  /  x ] ps ) )
3 sbanv 1814 . . 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 1462 . . 3  |-  ( (
ph  /\  ps )  ->  A. z ( ph  /\ 
ps ) )
65sbco2v 1866 . 2  |-  ( [ y  /  z ] [ z  /  x ] ( ph  /\  ps )  <->  [ y  /  x ] ( ph  /\  ps ) )
7 ax-17 1462 . . . 4  |-  ( ph  ->  A. z ph )
87sbco2v 1866 . . 3  |-  ( [ y  /  z ] [ z  /  x ] ph  <->  [ y  /  x ] ph )
9 ax-17 1462 . . . 4  |-  ( ps 
->  A. z ps )
109sbco2v 1866 . . 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 1689
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 1379  ax-7 1380  ax-gen 1381  ax-ie1 1425  ax-ie2 1426  ax-8 1438  ax-10 1439  ax-11 1440  ax-i12 1441  ax-4 1443  ax-17 1462  ax-i9 1466  ax-ial 1470  ax-i5r 1471
This theorem depends on definitions:  df-bi 115  df-nf 1393  df-sb 1690
This theorem is referenced by:  sb3an  1877  sbbi  1878  sbmo  2004  moanim  2019  sbabel  2250  nfrexdya  2409  cbvreu  2584  sbcan  2870  sbcang  2871  rmo3  2919  inab  3256  difab  3257  exss  4030  inopab  4538  bdcriota  11243
  Copyright terms: Public domain W3C validator