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

Theorem 4exbidv 1870
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 1868 . 2 (𝜑 → (∃𝑧𝑤𝜓 ↔ ∃𝑧𝑤𝜒))
322exbidv 1868 1 (𝜑 → (∃𝑥𝑦𝑧𝑤𝜓 ↔ ∃𝑥𝑦𝑧𝑤𝜒))
Colors of variables: wff set class
Syntax hints:  wi 4  wb 105  wex 1492
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 1447  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-4 1510  ax-17 1526  ax-ial 1534
This theorem depends on definitions:  df-bi 117
This theorem is referenced by:  ceqsex8v  2783  copsex4g  4248  opbrop  4706  ovi3  6011  brecop  6625  th3q  6640  dfplpq2  7353  dfmpq2  7354  enq0sym  7431  enq0ref  7432  enq0tr  7433  enq0breq  7435  addnq0mo  7446  mulnq0mo  7447  addnnnq0  7448  mulnnnq0  7449  addsrmo  7742  mulsrmo  7743  addsrpr  7744  mulsrpr  7745
  Copyright terms: Public domain W3C validator