Theorem gen2 1503

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

This proof depends on syntax axioms:  ∀wal 1400

This proof depends on axioms:  ax-gen 1502

This theorem is used by:  euequ1  2182  bm1.1  2223  vtocl3  2879  eueq  2997  csbie2  3197  moop2  4392  eusv1  4598  ordtriexmidlem  4666  ordtri2or2exmidlem  4673  onsucelsucexmidlem  4676  ordom  4754  mosubop  4841  eqrelriv  4868  opabid2  4911  xpidtr  5178  funinsn  5430  funoprab  6188  mpofun  6190  fnoprab  6191  elovmpo  6288  mpofvexi  6442  tfrlem7  6588  oaexg  6721  omexg  6724  oeiexg  6726  infiexmid  7181  domfiexmid  7182  climeu  12062  clwwlknon  16670