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

Theorem 4exbidv 1750
 Description: Formula-building rule for 4 existential quantifiers (deduction rule). (Contributed by NM, 3-Aug-1995.)
Hypothesis
Ref Expression
4exbidv.1
Assertion
Ref Expression
4exbidv
Distinct variable groups:   ,   ,   ,   ,
Allowed substitution hints:   (,,,)   (,,,)

Proof of Theorem 4exbidv
StepHypRef Expression
1 4exbidv.1 . . 3
212exbidv 1748 . 2
322exbidv 1748 1
 Colors of variables: wff set class Syntax hints:   wi 4   wb 98  wex 1381 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-5 1336  ax-gen 1338  ax-ie1 1382  ax-ie2 1383  ax-4 1400  ax-17 1419  ax-ial 1427 This theorem depends on definitions:  df-bi 110 This theorem is referenced by:  ceqsex8v  2599  copsex4g  3984  opbrop  4419  ovi3  5637  brecop  6196  th3q  6211  dfplpq2  6452  dfmpq2  6453  enq0sym  6530  enq0ref  6531  enq0tr  6532  enq0breq  6534  addnq0mo  6545  mulnq0mo  6546  addnnnq0  6547  mulnnnq0  6548  addsrmo  6828  mulsrmo  6829  addsrpr  6830  mulsrpr  6831
 Copyright terms: Public domain W3C validator