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

Theorem 4exbidv 1842
 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 1840 . 2 (𝜑 → (∃𝑧𝑤𝜓 ↔ ∃𝑧𝑤𝜒))
322exbidv 1840 1 (𝜑 → (∃𝑥𝑦𝑧𝑤𝜓 ↔ ∃𝑥𝑦𝑧𝑤𝜒))
 Colors of variables: wff set class Syntax hints:   → wi 4   ↔ wb 104  ∃wex 1468 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1423  ax-gen 1425  ax-ie1 1469  ax-ie2 1470  ax-4 1487  ax-17 1506  ax-ial 1514 This theorem depends on definitions:  df-bi 116 This theorem is referenced by:  ceqsex8v  2731  copsex4g  4169  opbrop  4618  ovi3  5907  brecop  6519  th3q  6534  dfplpq2  7169  dfmpq2  7170  enq0sym  7247  enq0ref  7248  enq0tr  7249  enq0breq  7251  addnq0mo  7262  mulnq0mo  7263  addnnnq0  7264  mulnnnq0  7265  addsrmo  7558  mulsrmo  7559  addsrpr  7560  mulsrpr  7561
 Copyright terms: Public domain W3C validator