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

Theorem 4exbidv 1747
 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 (φ → (xyzwψxyzwχ))
Distinct variable groups:   φ,x   φ,y   φ,z   φ,w
Allowed substitution hints:   ψ(x,y,z,w)   χ(x,y,z,w)

Proof of Theorem 4exbidv
StepHypRef Expression
1 4exbidv.1 . . 3 (φ → (ψχ))
212exbidv 1745 . 2 (φ → (zwψzwχ))
322exbidv 1745 1 (φ → (xyzwψxyzwχ))
 Colors of variables: wff set class Syntax hints:   → wi 4   ↔ wb 98  ∃wex 1378 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 1333  ax-gen 1335  ax-ie1 1379  ax-ie2 1380  ax-4 1397  ax-17 1416  ax-ial 1424 This theorem depends on definitions:  df-bi 110 This theorem is referenced by:  ceqsex8v  2593  copsex4g  3975  opbrop  4362  ovi3  5579  brecop  6132  th3q  6147  dfplpq2  6338  dfmpq2  6339  enq0sym  6414  enq0ref  6415  enq0tr  6416  enq0breq  6418  addnq0mo  6429  mulnq0mo  6430  addnnnq0  6431  mulnnnq0  6432  addsrmo  6651  mulsrmo  6652  addsrpr  6653  mulsrpr  6654
 Copyright terms: Public domain W3C validator