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

Theorem ax11inda 1818
Description: Induction step for constructing a substitution instance of ax-11o 1654 without using ax-11o 1654. Quantification case. (When and are distinct, ax11inda2 1817 may be used instead to avoid the dummy variable in the proof.)
Hypothesis
Ref Expression
ax11inda.1
Assertion
Ref Expression
ax11inda
Distinct variable groups:   ,   ,   ,   ,
Allowed substitution hints:   (,,)

Proof of Theorem ax11inda
StepHypRef Expression
1 a9e 1556 . . 3
2 ax11inda.1 . . . . . . 7
32ax11inda2 1817 . . . . . 6
4 dveeq2 1646 . . . . . . . . 9
54imp 114 . . . . . . . 8
6 hba1 1436 . . . . . . . . . 10
7 equequ2 1571 . . . . . . . . . . 11
87a4s 1433 . . . . . . . . . 10
96, 8albid 1360 . . . . . . . . 9
109notbid 571 . . . . . . . 8
115, 10syl 14 . . . . . . 7
127adantl 261 . . . . . . . 8
138imbi1d 219 . . . . . . . . . . 11
146, 13albid 1360 . . . . . . . . . 10
155, 14syl 14 . . . . . . . . 9
1615imbi2d 218 . . . . . . . 8
1712, 16imbi12d 222 . . . . . . 7
1811, 17imbi12d 222 . . . . . 6
193, 18mpbii 135 . . . . 5
2019ex 107 . . . 4
2120exlimdv 1650 . . 3
221, 21mpi 15 . 2
2322pm2.43i 42 1
Colors of variables: wff set class
Syntax hints:   wn 3   wi 4   wa 96   wb 97  wal 1335  wex 1374
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-ia1 98  ax-ia2 99  ax-ia3 100  ax-in1 527  ax-in2 528  ax-io 607  ax-5 1336  ax-6 1337  ax-7 1338  ax-gen 1339  ax-ie1 1375  ax-ie2 1376  ax-8 1387  ax-10 1388  ax-11 1389  ax-i12 1391  ax-4 1392  ax-17 1402  ax-i9 1417  ax-ial 1430  ax-i5r 1431  ax-16 1644
This theorem depends on definitions:  df-bi 109
  Copyright terms: Public domain W3C validator