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

Theorem 4exbidv 1880
Description: Formula-building rule for 4 existential quantifiers (deduction form). (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 1878 . 2 (𝜑 → (∃𝑧𝑤𝜓 ↔ ∃𝑧𝑤𝜒))
322exbidv 1878 1 (𝜑 → (∃𝑥𝑦𝑧𝑤𝜓 ↔ ∃𝑥𝑦𝑧𝑤𝜒))
Colors of variables: wff set class
Syntax hints:  wi 4  wb 105  wex 1502
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1457  ax-gen 1459  ax-ie1 1503  ax-ie2 1504  ax-4 1520  ax-17 1536  ax-ial 1544
This theorem depends on definitions:  df-bi 117
This theorem is referenced by:  ceqsex8v  2794  copsex4g  4259  opbrop  4717  ovi3  6025  brecop  6639  th3q  6654  dfplpq2  7367  dfmpq2  7368  enq0sym  7445  enq0ref  7446  enq0tr  7447  enq0breq  7449  addnq0mo  7460  mulnq0mo  7461  addnnnq0  7462  mulnnnq0  7463  addsrmo  7756  mulsrmo  7757  addsrpr  7758  mulsrpr  7759
  Copyright terms: Public domain W3C validator