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

Theorem sban 1929
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 1862 . . . 4  |-  ( [ z  /  x ]
( ph  /\  ps )  <->  ( [ z  /  x ] ph  /\  [ z  /  x ] ps ) )
21sbbii 1739 . . 3  |-  ( [ y  /  z ] [ z  /  x ] ( ph  /\  ps )  <->  [ y  /  z ] ( [ z  /  x ] ph  /\ 
[ z  /  x ] ps ) )
3 sbanv 1862 . . 3  |-  ( [ y  /  z ] ( [ z  /  x ] ph  /\  [
z  /  x ] ps )  <->  ( [ y  /  z ] [
z  /  x ] ph  /\  [ y  / 
z ] [ z  /  x ] ps ) )
42, 3bitri 183 . 2  |-  ( [ y  /  z ] [ z  /  x ] ( ph  /\  ps )  <->  ( [ y  /  z ] [
z  /  x ] ph  /\  [ y  / 
z ] [ z  /  x ] ps ) )
5 ax-17 1507 . . 3  |-  ( (
ph  /\  ps )  ->  A. z ( ph  /\ 
ps ) )
65sbco2vh 1919 . 2  |-  ( [ y  /  z ] [ z  /  x ] ( ph  /\  ps )  <->  [ y  /  x ] ( ph  /\  ps ) )
7 ax-17 1507 . . . 4  |-  ( ph  ->  A. z ph )
87sbco2vh 1919 . . 3  |-  ( [ y  /  z ] [ z  /  x ] ph  <->  [ y  /  x ] ph )
9 ax-17 1507 . . . 4  |-  ( ps 
->  A. z ps )
109sbco2vh 1919 . . 3  |-  ( [ y  /  z ] [ z  /  x ] ps  <->  [ y  /  x ] ps )
118, 10anbi12i 456 . 2  |-  ( ( [ y  /  z ] [ z  /  x ] ph  /\  [ y  /  z ] [
z  /  x ] ps )  <->  ( [ y  /  x ] ph  /\ 
[ y  /  x ] ps ) )
124, 6, 113bitr3i 209 1  |-  ( [ y  /  x ]
( ph  /\  ps )  <->  ( [ y  /  x ] ph  /\  [ y  /  x ] ps ) )
Colors of variables: wff set class
Syntax hints:    /\ wa 103    <-> wb 104   [wsb 1736
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 699  ax-5 1424  ax-7 1425  ax-gen 1426  ax-ie1 1470  ax-ie2 1471  ax-8 1483  ax-10 1484  ax-11 1485  ax-i12 1486  ax-4 1488  ax-17 1507  ax-i9 1511  ax-ial 1515  ax-i5r 1516
This theorem depends on definitions:  df-bi 116  df-nf 1438  df-sb 1737
This theorem is referenced by:  sb3an  1932  sbbi  1933  sbmo  2059  moanim  2074  sbabel  2308  nfrexdya  2473  cbvreu  2655  rmo3f  2884  sbcan  2954  sbcang  2955  rmo3  3003  inab  3348  difab  3349  exss  4156  inopab  4678  bdcriota  13250
  Copyright terms: Public domain W3C validator