Theorem gen2 1496

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

Syntax hints:  ∀wal 1393

This theorem was proved from axioms:  ax-gen 1495

This theorem is referenced by:  euequ1  2173  bm1.1  2214  vtocl3  2857  eueq  2974  csbie2  3174  moop2  4337  eusv1  4542  ordtriexmidlem  4610  ordtri2or2exmidlem  4617  onsucelsucexmidlem  4620  ordom  4698  mosubop  4784  eqrelriv  4811  opabid2  4852  xpidtr  5118  funinsn  5369  funoprab  6103  mpofun  6105  fnoprab  6106  elovmpo  6203  mpofvexi  6350  tfrlem7  6461  oaexg  6592  omexg  6595  oeiexg  6597  infiexmid  7035  domfiexmid  7036  climeu  11802