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

Theorem 4exbidv 1805
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 1803 . 2 (𝜑 → (∃𝑧𝑤𝜓 ↔ ∃𝑧𝑤𝜒))
322exbidv 1803 1 (𝜑 → (∃𝑥𝑦𝑧𝑤𝜓 ↔ ∃𝑥𝑦𝑧𝑤𝜒))
Colors of variables: wff set class
Syntax hints:  wi 4  wb 104  wex 1433
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1388  ax-gen 1390  ax-ie1 1434  ax-ie2 1435  ax-4 1452  ax-17 1471  ax-ial 1479
This theorem depends on definitions:  df-bi 116
This theorem is referenced by:  ceqsex8v  2678  copsex4g  4098  opbrop  4546  ovi3  5819  brecop  6422  th3q  6437  dfplpq2  7010  dfmpq2  7011  enq0sym  7088  enq0ref  7089  enq0tr  7090  enq0breq  7092  addnq0mo  7103  mulnq0mo  7104  addnnnq0  7105  mulnnnq0  7106  addsrmo  7386  mulsrmo  7387  addsrpr  7388  mulsrpr  7389
  Copyright terms: Public domain W3C validator