Theorem gen2 1336

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

Hypothesis

Ref	Expression
gen2.1	⊢ φ

Assertion

Ref	Expression
gen2	⊢ ∀x∀yφ

Proof of Theorem gen2

Step	Hyp	Ref	Expression
1		gen2.1	. . 3 ⊢ φ
2	1	ax-gen 1335	. 2 ⊢ ∀yφ
3	2	ax-gen 1335	1 ⊢ ∀x∀yφ

Syntax hints:  ∀wal 1240

This theorem was proved from axioms:  ax-gen 1335

This theorem is referenced by:  euequ1  1992  bm1.1  2022  vtocl3  2604  eueq  2706  csbie2  2889  moop2  3979  eusv1  4150  ordtriexmidlem  4208  onsucelsucexmidlem  4214  ordom  4272  mosubop  4349  eqrelriv  4376  opabid2  4410  xpidtr  4658  funoprab  5543  mpt2fun  5545  fnoprab  5546  elovmpt2  5643  mpt2fvexi  5774  tfrlem7  5874  oaexg  5967  omexg  5970  oeiexg  5972