Theorem 19.22i2 1037

Description: Inference adding 2 existential quantifiers to antecedent and consequent.

Hypothesis

Ref	Expression
19.22i.1	|- (ph -> ps)

Assertion

Ref	Expression
19.22i2	|- (E.xE.yph -> E.xE.yps)

Proof of Theorem 19.22i2

Step	Hyp	Ref	Expression
1		19.22i.1	. . 3 |- (ph -> ps)
2	1	19.22i 1036	. 2 |- (E.yph -> E.yps)
3	2	19.22i 1036	1 |- (E.xE.yph -> E.xE.yps)

Syntax hints:   -> wi 3  E.wex 977

This theorem is referenced by:  excomim 1041  2mo 1440  2eu6 1447  cgsex2g 1823  cgsex4g 1824  vtocl2 1834  vtocl3 1835  dtruALT 2738  mosubopt 2793  ralxp 3208  xpss 3220  ssoprab2i 3993  bsi 10382

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 960  ax-4 970  ax-5o 972

This theorem depends on definitions:  df-bi 147  df-an 225  df-ex 978

Copyright terms: Public domain