Theorem gen2 1828

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

This proof depends on syntax axioms:  ∀wal 1567

This proof depends on axioms:  ax-gen 1827

This theorem is used by:  axextmo  2736  moeq  3664  csbie2  3885  mosneq  4796  eusv1  5352  moop2  5473  mosubop  5482  eqrelriv  5764  opabid2  5805  xpidtr  6115  funoprab  7543  fnoprab  7546  elovmpo  7667  funmpt3  7688  mpt3fvd  7689  tfrlem7  8395  funen1cnv  9060  hartogs  9542  card2on  9552  epinid0  9603  cnvepnep  9613  ssttrcl  9720  tskwe  10035  ondomon  10651  fi1uzind  14656  brfi1indALT  14659  climeu  15728  letsr  18773  ulmdm  26726  ajmoi  31466  helch  31851  hsn0elch  31856  chintcli  31939  adjmo  32440  nlelchi  32669  hmopidmchi  32759  bnj978  35626  bnj1052  35652  bnj1030  35664  axsepg4  35868  satfv0  36210  satfv0fun  36223  fnsingle  36774  funimage  36783  funpartfun  36800  imagesset  36810  funtransport  36889  funray  36998  funline  37000  filnetlem3  37261  ttctr  37374  dfttc2g  37387  dfttc4lem2  37410  ax11-pm  37837  ax11-pm2  37841  bj-snsetex  37969  wl-equsal1i  38570  mbfresfi  38678  riscer  39016  vvdifopab  39291  opabf  39402  mopre  39497  cnvcosseq  39553  antisymressn  39560  trressn  39561  symrelcoss3  39581  cotrintab  44708  pm11.11  45452  fun2dmnopgexmpl  48448  ichv  48625  ichf  48626  ichid  48627  icht  48628  ichcircshi  48630  icheq  48638  pg4cyclnex  49319  mof0ALT  50045  f1omoOLD  50102