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

Theorem hbae 1424
Description: All variables are effectively bound in an identical variable specifier. (Contributed by NM, 5-Aug-1993.) (Revised by NM, 3-Feb-2015.)
Assertion
Ref Expression
hbae

Proof of Theorem hbae
StepHypRef Expression
1 ax12or 1272 . . . 4
2 ax10o 1421 . . . . . 6
32alequcoms 1277 . . . . 5
4 ax10o 1421 . . . . . . . . 9
54pm2.43i 41 . . . . . . . 8
6 ax10o 1421 . . . . . . . 8
75, 6syl5 26 . . . . . . 7
87alequcoms 1277 . . . . . 6
9 ax-4 1269 . . . . . . . 8
109imim1i 52 . . . . . . 7
1110a4s 1296 . . . . . 6
128, 11jaoi 612 . . . . 5
133, 12jaoi 612 . . . 4
141, 13ax-mp 7 . . 3
1514a5i 1301 . 2
16 ax-7 1206 . 2
1715, 16syl 13 1
Colors of variables: wff set class
Syntax hints:   wi 4   wo 605  wal 1204   wceq 1261
This theorem is referenced by:  nfae  1425  hbaes  1426  hbnae  1427  dral1  1435  dral2  1436  drex2  1437  sbequ5  1475  drex1  1486  aev  1500  hbsb4  1535  sbcom  1542  exists1  1770  a12stdy3  1851
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 97  ax-ia2 98  ax-ia3 99  ax-io 606  ax-5 1205  ax-7 1206  ax-gen 1207  ax-ie2 1253  ax-8 1265  ax-10 1266  ax-11 1267  ax-i12 1268  ax-4 1269  ax-17 1284  ax-i9 1288  ax-ial 1293
This theorem depends on definitions:  df-bi 108
  Copyright terms: Public domain W3C validator