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

Theorem iotabidv 4955
Description: Formula-building deduction rule for iota. (Contributed by NM, 20-Aug-2011.)
Hypothesis
Ref Expression
iotabidv.1  |-  ( ph  ->  ( ps  <->  ch )
)
Assertion
Ref Expression
iotabidv  |-  ( ph  ->  ( iota x ps )  =  ( iota
x ch ) )
Distinct variable group:    ph, x
Allowed substitution hints:    ps( x)    ch( x)

Proof of Theorem iotabidv
StepHypRef Expression
1 iotabidv.1 . . 3  |-  ( ph  ->  ( ps  <->  ch )
)
21alrimiv 1797 . 2  |-  ( ph  ->  A. x ( ps  <->  ch ) )
3 iotabi 4943 . 2  |-  ( A. x ( ps  <->  ch )  ->  ( iota x ps )  =  ( iota
x ch ) )
42, 3syl 14 1  |-  ( ph  ->  ( iota x ps )  =  ( iota
x ch ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 103   A.wal 1283    = wceq 1285   iotacio 4932
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 1377  ax-7 1378  ax-gen 1379  ax-ie1 1423  ax-ie2 1424  ax-8 1436  ax-10 1437  ax-11 1438  ax-i12 1439  ax-bndl 1440  ax-4 1441  ax-17 1460  ax-i9 1464  ax-ial 1468  ax-i5r 1469  ax-ext 2065
This theorem depends on definitions:  df-bi 115  df-tru 1288  df-nf 1391  df-sb 1688  df-clab 2070  df-cleq 2076  df-clel 2079  df-nfc 2212  df-rex 2359  df-uni 3628  df-iota 4934
This theorem is referenced by:  csbiotag  4962  dffv3g  5249  fveq1  5252  fveq2  5253  fvres  5274  csbfv12g  5285  fvco2  5318  riotaeqdv  5548  riotabidv  5549  riotabidva  5563  ovtposg  5956  shftval  10087  sumeq1  10566  sumeq2d  10570  sumeq2  10571
  Copyright terms: Public domain W3C validator