Theorem 19.22i2 1041

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 1040	. 2 |- (E.yph -> E.yps)
3	2	19.22i 1040	1 |- (E.xE.yph -> E.xE.yps)

Syntax hints:   -> wi 3  E.wex 980

This theorem is referenced by:  excomim 1045  2mo 1447  2eu6 1454  cgsex2g 1832  cgsex4g 1833  vtocl2 1843  vtocl3 1844  dtruALT 2748  mosubopt 2804  ralxp 3218  xpss 3230  ssoprab2i 4008  bsi 10495

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 963  ax-4 973  ax-5o 975

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

Copyright terms: Public domain