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

Theorem sban 1955
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 1889 . . . 4  |-  ( [ z  /  x ]
( ph  /\  ps )  <->  ( [ z  /  x ] ph  /\  [ z  /  x ] ps ) )
21sbbii 1765 . . 3  |-  ( [ y  /  z ] [ z  /  x ] ( ph  /\  ps )  <->  [ y  /  z ] ( [ z  /  x ] ph  /\ 
[ z  /  x ] ps ) )
3 sbanv 1889 . . 3  |-  ( [ y  /  z ] ( [ z  /  x ] ph  /\  [
z  /  x ] ps )  <->  ( [ y  /  z ] [
z  /  x ] ph  /\  [ y  / 
z ] [ z  /  x ] ps ) )
42, 3bitri 184 . 2  |-  ( [ y  /  z ] [ z  /  x ] ( ph  /\  ps )  <->  ( [ y  /  z ] [
z  /  x ] ph  /\  [ y  / 
z ] [ z  /  x ] ps ) )
5 ax-17 1526 . . 3  |-  ( (
ph  /\  ps )  ->  A. z ( ph  /\ 
ps ) )
65sbco2vh 1945 . 2  |-  ( [ y  /  z ] [ z  /  x ] ( ph  /\  ps )  <->  [ y  /  x ] ( ph  /\  ps ) )
7 ax-17 1526 . . . 4  |-  ( ph  ->  A. z ph )
87sbco2vh 1945 . . 3  |-  ( [ y  /  z ] [ z  /  x ] ph  <->  [ y  /  x ] ph )
9 ax-17 1526 . . . 4  |-  ( ps 
->  A. z ps )
109sbco2vh 1945 . . 3  |-  ( [ y  /  z ] [ z  /  x ] ps  <->  [ y  /  x ] ps )
118, 10anbi12i 460 . 2  |-  ( ( [ y  /  z ] [ z  /  x ] ph  /\  [ y  /  z ] [
z  /  x ] ps )  <->  ( [ y  /  x ] ph  /\ 
[ y  /  x ] ps ) )
124, 6, 113bitr3i 210 1  |-  ( [ y  /  x ]
( ph  /\  ps )  <->  ( [ y  /  x ] ph  /\  [ y  /  x ] ps ) )
Colors of variables: wff set class
Syntax hints:    /\ wa 104    <-> wb 105   [wsb 1762
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 709  ax-5 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-10 1505  ax-11 1506  ax-i12 1507  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535
This theorem depends on definitions:  df-bi 117  df-nf 1461  df-sb 1763
This theorem is referenced by:  sb3an  1958  sbbi  1959  sbmo  2085  moanim  2100  sbabel  2346  nfrexdya  2513  cbvreu  2701  rmo3f  2934  sbcan  3005  sbcang  3006  rmo3  3054  inab  3403  difab  3404  exss  4223  inopab  4754  bdcriota  14257
  Copyright terms: Public domain W3C validator