Theorem gen2 1329

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

Syntax hints:  A.wal 1296

This theorem is referenced by:  euequ1 1861  bm1.1 1870  vtocl3 2342  vtocl3OLD 2343  eueq 2427  csbie2 2579  csbco3g 2585  sbcco3g 2586  moop2 3548  mosubop 3552  eualeq 3823  euexeqOLD 3826  eqrelriv 4080  opabid2 4107  dfrel2 4358  coi1 4413  funsnOLD 4464  funoprab 4940  fnoprab 4942  fparlem3 5083  fparlem4 5084  tfrlem7 5125  ster 5325  ordtypelem5 5688  hartog 5693  ondomon 6008  climeu 8360  ajmoi 9860  hlimeui 10744  helch 10749  hsn0elch 10753  occli 10814  chintcli 10928  osumlem7 11219  adjmo 11395  nlelchi 11631  bra11 11679  hmopidmchi 11723  bnj1036 12886  bnj978 13355  mpt2fun 13843  wfrlem11 13967  fnbigcup 14075  cpref 14379  fgsb 14921  fgsb2 14925  lteqtpos 15024  ordtypelem5OLD 15379  hartogOLD 15384  fneer 15496  pm11.11 16323

This theorem was proved from axioms:  ax-gen 1305

Copyright terms: Public domain