Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  iotabii Unicode version

Theorem iotabii 5578
 Description: Formula-building deduction rule for iota. (Contributed by Mario Carneiro, 2-Oct-2015.)
Hypothesis
Ref Expression
iotabii.1
Assertion
Ref Expression
iotabii

Proof of Theorem iotabii
StepHypRef Expression
1 iotabi 5565 . 2
2 iotabii.1 . 2
31, 2mpg 1620 1
 Colors of variables: wff setvar class Syntax hints:  <->wb 184  =wceq 1395  iotacio 5554 This theorem is referenced by:  riotav  6262  ovtpos  6989  cbvsum  13517  cbvprod  13722  oppgid  16391  oppr1  17283  fourierdlem89  31978  fourierdlem90  31979  fourierdlem91  31980  fourierdlem96  31985  fourierdlem97  31986  fourierdlem98  31987  fourierdlem99  31988  fourierdlem100  31989  fourierdlem112  32001 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435 This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-rex 2813  df-uni 4250  df-iota 5556
 Copyright terms: Public domain W3C validator