Theorem gen2 980

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 960	. 2 |- A.yph
3	2	ax-gen 960	1 |- A.xA.yph

Syntax hints:  A.wal 951

This theorem is referenced by:  bm1.1 1455  vtocl3 1835  eueq 1907  csbie2 2024  csbco3g 2030  sbcco3g 2031  moop2 2790  mosubop 2794  opabid2 3257  dfrel2 3471  coi1 3496  funsn 3529  tfrlem7 3902  funoprab 3996  fnoprab 3998  ster 4252  ondomon 4828  climeu 7037  ajmoi 8450  hlimeu 9032  helch 9037  hsn0elch 9041  occl 9097  chintcl 9210  osumlem7 9501  adjmo 9675  nlelch 9909  bra11 9954  hmopidmch 9990  fgsb 10444  fgsb2 10449

This theorem was proved from axioms:  ax-gen 960

Copyright terms: Public domain