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

Theorem 2exbidv 1822
Description: Formula-building rule for 2 existential quantifiers (deduction form). (Contributed by NM, 1-May-1995.)
Hypothesis
Ref Expression
2albidv.1  |-  ( ph  ->  ( ps  <->  ch )
)
Assertion
Ref Expression
2exbidv  |-  ( ph  ->  ( E. x E. y ps  <->  E. x E. y ch ) )
Distinct variable groups:    ph, x    ph, y
Allowed substitution hints:    ps( x, y)    ch( x, y)

Proof of Theorem 2exbidv
StepHypRef Expression
1 2albidv.1 . . 3  |-  ( ph  ->  ( ps  <->  ch )
)
21exbidv 1779 . 2  |-  ( ph  ->  ( E. y ps  <->  E. y ch ) )
32exbidv 1779 1  |-  ( ph  ->  ( E. x E. y ps  <->  E. x E. y ch ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 104   E.wex 1451
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 1406  ax-gen 1408  ax-ie1 1452  ax-ie2 1453  ax-4 1470  ax-17 1489  ax-ial 1497
This theorem depends on definitions:  df-bi 116
This theorem is referenced by:  3exbidv  1823  4exbidv  1824  cbvex4v  1880  ceqsex3v  2700  ceqsex4v  2701  copsexg  4134  euotd  4144  elopab  4148  elxpi  4523  relop  4657  cbvoprab3  5813  ov6g  5874  th3qlem1  6497  ltresr  7611  fisumcom2  11147
  Copyright terms: Public domain W3C validator