Theorem gen2 959

Description: Generalization applied twice.

Hypothesis

Ref	Expression
gen2.1	|- ph

Assertion

Ref	Expression
gen2	|- A.xA.yph

Proof of Theorem gen2

Step	Hyp	Ref	Expression
1		gen2.1	. . 3 |- ph
2	1	ax-gen 955	. 2 |- A.yph
3	2	ax-gen 955	1 |- A.xA.yph

Syntax hints:  A.wal 950

This theorem is referenced by:  bm1.1 1439  vtocl3 1819  eueq 1888  csbie2 2005  csbco3g 2011  sbcco3g 2012  moop2 2766  mosubop 2768  opabid2 3229  dfrel2 3431  coi1 3452  funsn 3484  tfrlem7 3856  funoprab 3950  fnoprab 3952  ster 4206  ondomon 4779  climeu 6988  ajmoi 8385  fgsb 8794  fgsb2 8799  hlimeu 9262  helch 9267  hsn0elch 9271  occl 9311  chintcl 9424  osumlem7 9715  adjmo 9889  nlelch 10123  bra11 10168  hmopidmch 10204

This theorem was proved from axioms:  ax-gen 955

Copyright terms: Public domain