Theorem gen2 1382

Description: Generalization applied twice. (Contributed by NM, 30-Apr-1998.)

Hypothesis

Ref	Expression
gen2.1	⊢ 𝜑

Assertion

Ref	Expression
gen2	⊢ ∀𝑥∀𝑦𝜑

Proof of Theorem gen2

Step	Hyp	Ref	Expression
1		gen2.1	. . 3 ⊢ 𝜑
2	1	ax-gen 1381	. 2 ⊢ ∀𝑦𝜑
3	2	ax-gen 1381	1 ⊢ ∀𝑥∀𝑦𝜑

Syntax hints:  ∀wal 1285

This theorem was proved from axioms:  ax-gen 1381

This theorem is referenced by:  euequ1  2040  bm1.1  2070  vtocl3  2669  eueq  2777  csbie2  2966  moop2  4054  eusv1  4250  ordtriexmidlem  4311  ordtri2or2exmidlem  4317  onsucelsucexmidlem  4320  ordom  4396  mosubop  4474  eqrelriv  4501  opabid2  4537  xpidtr  4791  funinsn  5030  funoprab  5704  mpt2fun  5706  fnoprab  5707  elovmpt2  5804  mpt2fvexi  5935  tfrlem7  6038  oaexg  6165  omexg  6168  oeiexg  6170  infiexmid  6547  domfiexmid  6548  climeu  10600