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  4338  eusv1  4543  ordtriexmidlem  4611  ordtri2or2exmidlem  4618  onsucelsucexmidlem  4621  ordom  4699  mosubop  4785  eqrelriv  4812  opabid2  4853  xpidtr  5119  funinsn  5370  funoprab  6110  mpofun  6112  fnoprab  6113  elovmpo  6210  mpofvexi  6358  tfrlem7  6469  oaexg  6602  omexg  6605  oeiexg  6607  infiexmid  7047  domfiexmid  7048  climeu  11822