Theorem gen2 1015

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

Syntax hints:  A.wal 986

This theorem is referenced by:  euequ1 1491  bm1.1 1498  vtocl3 1882  eueq 1954  csbie2 2078  csbco3g 2084  sbcco3g 2085  moop2 2854  mosubop 2858  opabid2 3333  dfrel2 3540  coi1 3584  funsn 3618  tfrlem7 3993  funoprab 4088  fnoprab 4090  ster 4352  ondomon 4945  climeu 7223  ajmoi 8638  hlimeui 9231  helch 9236  hsn0elch 9240  occli 9301  chintcli 9415  osumlem7 9704  adjmo 9878  nlelchi 10111  bra11 10158  hmopidmchi 10196  fgsb 10708  fgsb2 10713

This theorem was proved from axioms:  ax-gen 995

Copyright terms: Public domain