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

Theorem 4exbidv 1766
 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 (𝜑 → (∃𝑥𝑦𝑧𝑤𝜓 ↔ ∃𝑥𝑦𝑧𝑤𝜒))
Distinct variable groups:   𝜑,𝑥   𝜑,𝑦   𝜑,𝑧   𝜑,𝑤
Allowed substitution hints:   𝜓(𝑥,𝑦,𝑧,𝑤)   𝜒(𝑥,𝑦,𝑧,𝑤)

Proof of Theorem 4exbidv
StepHypRef Expression
1 4exbidv.1 . . 3 (𝜑 → (𝜓𝜒))
212exbidv 1764 . 2 (𝜑 → (∃𝑧𝑤𝜓 ↔ ∃𝑧𝑤𝜒))
322exbidv 1764 1 (𝜑 → (∃𝑥𝑦𝑧𝑤𝜓 ↔ ∃𝑥𝑦𝑧𝑤𝜒))
 Colors of variables: wff set class Syntax hints:   → wi 4   ↔ wb 102  ∃wex 1397 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 103  ax-ia2 104  ax-ia3 105  ax-5 1352  ax-gen 1354  ax-ie1 1398  ax-ie2 1399  ax-4 1416  ax-17 1435  ax-ial 1443 This theorem depends on definitions:  df-bi 114 This theorem is referenced by:  ceqsex8v  2616  copsex4g  4012  opbrop  4447  ovi3  5665  brecop  6227  th3q  6242  dfplpq2  6510  dfmpq2  6511  enq0sym  6588  enq0ref  6589  enq0tr  6590  enq0breq  6592  addnq0mo  6603  mulnq0mo  6604  addnnnq0  6605  mulnnnq0  6606  addsrmo  6886  mulsrmo  6887  addsrpr  6888  mulsrpr  6889
 Copyright terms: Public domain W3C validator