Theorem gen2 1450

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 1449	. 2 ⊢ ∀𝑦𝜑
3	2	ax-gen 1449	1 ⊢ ∀𝑥∀𝑦𝜑

Syntax hints:  ∀wal 1351

This theorem was proved from axioms:  ax-gen 1449

This theorem is referenced by:  euequ1  2121  bm1.1  2162  vtocl3  2794  eueq  2909  csbie2  3107  moop2  4252  eusv1  4453  ordtriexmidlem  4519  ordtri2or2exmidlem  4526  onsucelsucexmidlem  4529  ordom  4607  mosubop  4693  eqrelriv  4720  opabid2  4759  xpidtr  5020  funinsn  5266  funoprab  5975  mpofun  5977  fnoprab  5978  elovmpo  6072  mpofvexi  6207  tfrlem7  6318  oaexg  6449  omexg  6452  oeiexg  6454  infiexmid  6877  domfiexmid  6878  climeu  11304